diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 77 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 92 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg (renamed from plugins/funind/g_indfun.ml4) | 144 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 34 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 35 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 86 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 5 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 96 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 28 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 59 | ||||
| -rw-r--r-- | plugins/funind/invfun.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/plugin_base.dune | 5 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 85 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 2 |
16 files changed, 359 insertions, 399 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index d04887a489..ef1d1af199 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -131,8 +131,7 @@ let finish_proof dynamic_infos g = g -let refine c = - Tacmach.refine c +let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) let thin l = Proofview.V82.of_tactic (Tactics.clear l) @@ -229,10 +228,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t = true with Not_found -> false -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty - - exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = @@ -243,7 +238,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Evarconv.e_conv env (ref sigma) c1 c2 in + let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; @@ -414,13 +409,13 @@ let rewrite_until_var arg_num eq_ids : tactic = let rec_pte_id = Id.of_string "Hrec" let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = - let coq_False = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ()) in - let coq_True = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ()) in - let coq_I = EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) in + let coq_False = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type") in + let coq_True = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.type") in + let coq_I = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in let rec scan_type context type_of_hyp : tactic = if isLetIn sigma type_of_hyp then let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in - let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in + let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in (* length of context didn't change ? *) let new_context,new_typ_of_hyp = decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp @@ -598,7 +593,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) - tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps; + tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in @@ -638,11 +633,11 @@ let my_orelse tac1 tac2 g = (* observe (str "using snd tac since : " ++ CErrors.print e); *) tac2 g -let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = +let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let args = Array.of_list (List.map mkVar args_id) in - let instanciate_one_hyp hid = + let instantiate_one_hyp hid = my_orelse - ( (* we instanciate the hyp if possible *) + ( (* we instantiate the hyp if possible *) fun g -> let prov_hid = pf_get_new_id hid g in let c = mkApp(mkVar hid,args) in @@ -678,7 +673,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = tclTHENLIST [ tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps; - tclMAP instanciate_one_hyp hyps; + tclMAP instantiate_one_hyp hyps; (fun g -> let all_g_hyps_id = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty @@ -722,11 +717,11 @@ let build_proof tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); (fun g' -> let g'_nb_prod = nb_prod (project g') (pf_concl g') in - let nb_instanciate_partial = g'_nb_prod - g_nb_prod in + let nb_instantiate_partial = g'_nb_prod - g_nb_prod in observe_tac "treat_new_case" (treat_new_case ptes_infos - nb_instanciate_partial + nb_instantiate_partial (build_proof do_finalize) t dyn_infos) @@ -760,7 +755,7 @@ let build_proof nb_rec_hyps = List.length new_hyps } in -(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' +(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g' (* build_proof do_finalize new_infos g' *) ) g | _ -> @@ -800,7 +795,7 @@ let build_proof g | LetIn _ -> let new_infos = - { dyn_infos with info = nf_betaiotazeta dyn_infos.info } + { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in tclTHENLIST @@ -834,7 +829,7 @@ let build_proof | LetIn _ -> let new_infos = { dyn_infos with - info = nf_betaiotazeta dyn_infos.info + info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info } in @@ -977,7 +972,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "body " ++ pr_lconstr bodies.(num)); *) let f_body_with_params_and_other_fun = substl fnames_with_params bodies.(num) in (* observe (str "f_body_with_params_and_other_fun " ++ pr_lconstr f_body_with_params_and_other_fun); *) - let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in + let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in (* observe (str "eq_rhs " ++ pr_lconstr eq_rhs); *) let (type_ctxt,type_of_f),evd = let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f @@ -1008,12 +1003,12 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) (mk_equation_id f_id) - (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem)) evd lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); + Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))); evd @@ -1050,9 +1045,9 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a (Global.env ()) !evd (Constrintern.locate_reference (qualid_of_ident equation_lemma_id)) in - let res = EConstr.of_constr res in - evd:=evd'; - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in + evd:=evd'; + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in + evd := sigma; res in let nb_intro_to_do = nb_prod (project g) (pf_concl g) in @@ -1099,10 +1094,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let get_body const = match Global.body_of_constant const with | Some (body, _) -> + let env = Global.env () in + let sigma = Evd.from_env env in Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - (Global.env ()) - (Evd.empty) + env + sigma (EConstr.of_constr body) | None -> user_err Pp.(str "Cannot define a principle over an axiom ") in @@ -1118,7 +1115,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in (full_params, (* real params *) princ_params, (* the params of the principle which are not params of the function *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl full_params) f_body ) @@ -1128,7 +1125,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let f_body = compose_lam f_ctxt_other f_body in (princ_info.params, (* real params *) [],(* all params are full params *) - substl (* function instanciated with real params *) + substl (* function instantiated with real params *) (List.map var_of_decl princ_info.params) f_body ) @@ -1242,7 +1239,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam if this_fix_info.idx + 1 = 0 then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *) else - observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1))) + observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1))) else Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1) other_fix_infos 0) @@ -1319,7 +1316,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *) (* ); *) - (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac + (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id)) ] @@ -1340,7 +1337,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam nb_rec_hyps = -100; rec_hyps = []; info = - Reductionops.nf_betaiota (pf_env g) Evd.empty + Reductionops.nf_betaiota (pf_env g) (project g) (applist(fbody_with_full_params, (List.rev_map var_of_decl princ_params)@ (List.rev_map mkVar args_id) @@ -1369,7 +1366,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam do_prove dyn_infos in - instanciate_hyps_with_args prove_tac + instantiate_hyps_with_args prove_tac (List.rev_map id_of_decl princ_info.branches) (List.rev args_id) ] @@ -1489,7 +1486,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, Lazy.force refl_equal))] - [Hints.Hint_db.empty empty_transparent_state false] + [Hints.Hint_db.empty TransparentState.empty false] ) ) ) @@ -1603,7 +1600,7 @@ let prove_principle_for_gen match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") | Value lemma -> EConstr.of_constr lemma - | Not_needed -> EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_I ()) + | Not_needed -> EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.True.I") in (* let rec list_diff del_list check_list = *) (* match del_list with *) @@ -1657,7 +1654,7 @@ let prove_principle_for_gen (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) (* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1))); + (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); @@ -1726,8 +1723,8 @@ let prove_principle_for_gen ptes_info (body_info rec_hyps) in - (* observe_tac "instanciate_hyps_with_args" *) - (instanciate_hyps_with_args + (* observe_tac "instantiate_hyps_with_args" *) + (instantiate_hyps_with_args make_proof (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 7a9bbd92cf..5ba9735690 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + open Printer open CErrors open Term @@ -266,7 +276,7 @@ let change_property_sort evd toSort princ princName = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in let init = let nargs = (princ_info.nparams + (List.length princ_info.predicates)) in - mkApp(princName_as_constr, + mkApp(EConstr.Unsafe.to_constr princName_as_constr, Array.init nargs (fun i -> mkRel (nargs - i ))) in @@ -291,12 +301,13 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin let new_princ_name = next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in + evd := sigma; let hook = Lemmas.mk_hook (hook new_principle_type) in begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) !evd (EConstr.of_constr new_principle_type) hook @@ -309,10 +320,16 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - get_proof_clean true, CEphemeron.create hook - end - + let open Proof_global in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) in + match entries with + | [entry] -> + discard_current (); + (id,(entry,persistence)), CEphemeron.create hook + | _ -> + CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") + end let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof @@ -321,8 +338,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let env = Global.env () in - let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in + let sigma, type_sort = Evd.fresh_sort_in_family !evd InType in + evd := sigma; let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -343,17 +360,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let evd',s = Evd.fresh_sort_in_family evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let univs = - let poly = Flags.is_universe_polymorphism () in - Evd.const_univ_entry ~poly evd' - in + let univs = Evd.const_univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in - ignore( + ignore( Declare.declare_constant name (DefinitionEntry ce, @@ -394,7 +408,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) exception Not_Rec -let get_funs_constant mp dp = +let get_funs_constant mp = let get_funs_constant const e : (Names.Constant.t*int) array = match Constr.kind ((strip_lam e)) with | Fix((_,(na,_,_))) -> @@ -402,7 +416,7 @@ let get_funs_constant mp dp = (fun i na -> match na with | Name id -> - let const = Constant.make3 mp dp (Label.of_id id) in + let const = Constant.make2 mp (Label.of_id id) in const,i | Anonymous -> anomaly (Pp.str "Anonymous fix.") @@ -474,13 +488,13 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in - let funs_mp,funs_dp,_ = KerName.repr (Constant.canonical (fst first_fun)) in + let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in let first_fun_kn = try fst (find_Function_infos (fst first_fun)).graph_ind with Not_found -> raise No_graph_found in - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp (fst first_fun) in + let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in let prop_sort = InProp in let funs_indexes = @@ -507,8 +521,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x - ) + let sigma, fs = Evd.fresh_sort_in_family !evd x in + evd := sigma; fs + ) fas in (* We create the first priciple by tactic *) @@ -626,18 +641,25 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in - let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in + let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in - let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in - (destConst f,sort) - ) + let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in + evd := sigma; + let c, u = + try EConstr.destConst !evd f + with DestKO -> + user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function") + in + (c, EConstr.EInstance.kind !evd u), sort + ) fas ) in let bodies_types = make_scheme evd pconstants in + List.iter2 (fun (princ_id,_,_) def_entry -> ignore @@ -657,19 +679,23 @@ let build_case_scheme fa = (* in *) let funs = let (_,f,_) = fa in - try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) + try (let open GlobRef in + match Smartlocate.global_with_alias f with + | ConstRef c -> c + | IndRef _ | ConstructRef _ | VarRef _ -> assert false) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in - let first_fun,u = destConst funs in - let funs_mp,funs_dp,_ = Constant.repr3 first_fun in + (str "Cannot find " ++ Libnames.pr_qualid f) in + let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in + let first_fun = funs in + let funs_mp = Constant.modpath first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in - let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in + let this_block_funs_indexes = get_funs_constant funs_mp first_fun in let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes + List.assoc_f Constant.equal funs this_block_funs_indexes in let (ind, sf) = let ind = first_fun_kn,funs_indexes in @@ -681,7 +707,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family x + fst @@ UnivGen.fresh_sort_in_family x ) fa in @@ -699,7 +725,7 @@ let build_case_scheme fa = (Some princ_name) this_block_funs 0 - (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|]) + (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|]) in () diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef81..97f9acdb3a 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.mlg index 90af20b4ca..8f0440a2a4 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.mlg @@ -7,22 +7,28 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) + +{ + open Ltac_plugin open Util open Pp open Constrexpr open Indfun_common open Indfun -open Genarg open Stdarg -open Misctypes -open Pcoq +open Tacarg +open Tactypes open Pcoq.Prim open Pcoq.Constr open Pltac +} + DECLARE PLUGIN "recdef_plugin" +{ + let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () @@ -38,29 +44,32 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> - let (_, b) = b (Global.env ()) Evd.empty in + let env = Global.env () in + let evd = Evd.from_env env in + let (_, b) = b env evd in spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) +} ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option - PRINTED BY pr_fun_ind_using_typed - RAW_TYPED AS constr_with_bindings_opt - RAW_PRINTED BY pr_fun_ind_using - GLOB_TYPED AS constr_with_bindings_opt - GLOB_PRINTED BY pr_fun_ind_using -| [ "using" constr_with_bindings(c) ] -> [ Some c ] -| [ ] -> [ None ] + PRINTED BY { pr_fun_ind_using_typed } + RAW_PRINTED BY { pr_fun_ind_using } + GLOB_PRINTED BY { pr_fun_ind_using } +| [ "using" constr_with_bindings(c) ] -> { Some c } +| [ ] -> { None } END TACTIC EXTEND newfuninv - [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> - [ +| [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] -> + { Proofview.V82.tactic (Invfun.invfun hyp fname) - ] + } END +{ + let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> @@ -72,58 +81,71 @@ let out_disjunctive = CAst.map (function | IntroAction (IntroOrAndPattern l) -> l | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")) -ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat -| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] -| [] ->[ None ] +} + +ARGUMENT EXTEND with_names TYPED AS intropattern option PRINTED BY { pr_intro_as_pat } +| [ "as" simple_intropattern(ipat) ] -> { Some ipat } +| [] -> { None } END +{ + let functional_induction b c x pat = Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat)) +} TACTIC EXTEND newfunind - ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ +| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + { let c = match cl with | [] -> assert false | [c] -> c | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl } END (***** debug only ***) TACTIC EXTEND snewfunind - ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> - [ +| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> + { let c = match cl with | [] -> assert false | [c] -> c | c::cl -> EConstr.applist(c,cl) in - Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl } END +{ let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc +} + ARGUMENT EXTEND constr_comma_sequence' - TYPED AS constr_list - PRINTED BY pr_constr_comma_sequence -| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ] -| [ constr(c) ] -> [ [c] ] + TYPED AS constr list + PRINTED BY { pr_constr_comma_sequence } +| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l } +| [ constr(c) ] -> { [c] } END +{ + let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc +} + ARGUMENT EXTEND auto_using' - TYPED AS constr_list - PRINTED BY pr_auto_using -| [ "using" constr_comma_sequence'(l) ] -> [ l ] -| [ ] -> [ [] ] + TYPED AS constr list + PRINTED BY { pr_auto_using } +| [ "using" constr_comma_sequence'(l) ] -> { l } +| [ ] -> { [] } END -module Gram = Pcoq.Gram -module Vernac = Pcoq.Vernac_ +{ + +module Vernac = Pvernac.Vernac_ module Tactic = Pltac type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located @@ -134,65 +156,77 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar let function_rec_definition_loc = Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) -GEXTEND Gram +} + +GRAMMAR EXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]] + [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]] ; END +{ + let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer +} + (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function - ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => [ let hard = List.exists (function +| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] + => { let hard = List.exists (function | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with - | Vernacexpr.VtSideff ids, _ when hard -> - Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) - | x -> x ] - -> [ do_generate_principle false (List.map snd recsl) ] + | Vernacextend.VtSideff ids, _ when hard -> + Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + | x -> x } + -> { do_generate_principle false (List.map snd recsl) } END +{ + let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Termops.pr_sort_family s + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ + Sorts.pr_sort_family s + +} VERNAC ARGUMENT EXTEND fun_scheme_arg -PRINTED BY pr_fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ] +PRINTED BY { pr_fun_scheme_arg } +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> { (princ_name,fun_name,s) } END +{ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e +} VERNAC COMMAND EXTEND NewFunctionalScheme - ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] - => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ] +| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] + => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - [ + { begin try Functional_principles_types.build_scheme fas @@ -220,17 +254,17 @@ VERNAC COMMAND EXTEND NewFunctionalScheme warning_error names e end - ] + } END (***** debug only ***) VERNAC COMMAND EXTEND NewFunctionalCase - ["Functional" "Case" fun_scheme_arg(fas) ] - => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ] - -> [ Functional_principles_types.build_case_scheme fas ] +| ["Functional" "Case" fun_scheme_arg(fas) ] + => { Vernacextend.(VtSideff[pi1 fas], VtLater) } + -> { Functional_principles_types.build_case_scheme fas } END (***** debug only ***) VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY -["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] +| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) } END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 49f7aae435..98aaa081c3 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -10,7 +10,6 @@ open Indfun_common open CErrors open Util open Glob_termops -open Misctypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -260,11 +259,8 @@ let mk_result ctxt value avoid = Some functions to deal with overlapping patterns **************************************************) -let coq_True_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "True") - -let coq_False_ref = - lazy (Coqlib.coq_reference "" ["Init";"Logic"] "False") +let coq_True_ref = lazy (Coqlib.lib_ref "core.True.type") +let coq_False_ref = lazy (Coqlib.lib_ref "core.False.type") (* [make_discr_match_el \[e1,...en\]] builds match e1,...,en with @@ -591,7 +587,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) build_entry_lc env funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") - | GProj _ -> user_err Pp.(str "Funind does not support primitive projections") | GProd _ -> user_err Pp.(str "Cannot apply a type") end (* end of the application treatement *) @@ -697,7 +692,6 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> build_entry_lc env funnames avoid b - | GProj(_,_) -> user_err Pp.(str "Funind does not support primitive projections") and build_entry_lc_from_case env funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : @@ -885,7 +879,7 @@ let is_res r = match DAst.get r with | _ -> false let is_gr c gr = match DAst.get c with -| GRef (r, _) -> Globnames.eq_gr r gr +| GRef (r, _) -> GlobRef.equal r gr | _ -> false let is_gvar c = match DAst.get c with @@ -894,7 +888,7 @@ let is_gvar c = match DAst.get c with let same_raw_term rt1 rt2 = match DAst.get rt1, DAst.get rt2 with - | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 + | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2 | GHole _, GHole _ -> true | _ -> false let decompose_raw_eq lhs rhs = @@ -960,7 +954,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = assert false end | GApp(eq_as_ref,[ty; id ;rt]) - when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gvar id && is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> let loc1 = rt.CAst.loc in let loc2 = eq_as_ref.CAst.loc in @@ -1081,7 +1075,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else new_b, Id.Set.add id id_to_exclude *) | GApp(eq_as_ref,[ty;rt1;rt2]) - when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + when is_gr eq_as_ref Coqlib.(lib_ref "core.eq.type") && n == Anonymous -> begin try @@ -1092,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef Coqlib.(lib_ref "core.eq.type"),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1247,7 +1241,7 @@ let rec compute_cst_params relnames params gt = DAst.with_val (function discrimination ones *) | GSort _ -> params | GHole _ -> params - | GIf _ | GRec _ | GCast _ | GProj _ -> + | GIf _ | GRec _ | GCast _ -> raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = @@ -1470,7 +1464,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((CAst.make @@ relnames.(i)), None), + ((CAst.make @@ relnames.(i)), rel_params, Some rel_arities.(i), ext_rel_constructors),[] @@ -1500,19 +1494,19 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ msg in @@ -1522,12 +1516,12 @@ let do_build_inductive let _time3 = System.get_time () in (* Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *) let repacked_rel_inds = - List.map (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) + List.map (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn ) rel_inds in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(GlobalNonCumulativity,false,Declarations.Finite,repacked_rel_inds))) + Ppvernac.pr_vernac Vernacexpr.(VernacExpr([], VernacInductive(None,false,Declarations.Finite,repacked_rel_inds))) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 40ea40b6b3..5b45a8dbed 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,10 +1,10 @@ open Pp +open Constr open Glob_term open CErrors open Util open Names open Decl_kinds -open Misctypes (* Some basic functions to rebuild glob_constr @@ -16,8 +16,8 @@ let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) (* Some basic functions to decompose glob_constrs @@ -38,11 +38,11 @@ let glob_decompose_app = (* [glob_make_eq t1 t2] build the glob_constr corresponding to [t2 = t1] *) let glob_make_eq ?(typ= mkGHole ()) t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_eq_ref),[typ;t2;t1]) + mkGApp(mkGRef (Coqlib.lib_ref "core.eq.type"),[typ;t2;t1]) (* [glob_make_neq t1 t2] build the glob_constr corresponding to [t1 <> t2] *) let glob_make_neq t1 t2 = - mkGApp(mkGRef (Lazy.force Coqlib.coq_not_ref),[glob_make_eq t1 t2]) + mkGApp(mkGRef (Coqlib.lib_ref "core.not.type"),[glob_make_eq t1 t2]) let remove_name_from_mapping mapping na = match na with @@ -108,8 +108,7 @@ let change_vars = | GHole _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, - Miscops.map_cast_type (change_vars mapping) c) - | GProj(p,c) -> GProj(p, change_vars mapping c) + Glob_ops.map_cast_type (change_vars mapping) c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = let new_mapping = List.fold_right Id.Map.remove idl mapping in @@ -289,12 +288,11 @@ let rec alpha_rt excluded rt = | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, - Miscops.map_cast_type (alpha_rt excluded) c) + Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp(f,args) -> GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args ) - | GProj(p,c) -> GProj(p, alpha_rt excluded c) in new_rt @@ -346,7 +344,6 @@ let is_free_in id = | GHole _ -> false | GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t | GCast (b,CastCoerce) -> is_free_in b - | GProj (_,c) -> is_free_in c ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -439,9 +436,7 @@ let replace_var_by_term x_id term = | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, - Miscops.map_cast_type replace_var_by_pattern c) - | GProj(p,c) -> - GProj(p,replace_var_by_pattern c) + Glob_ops.map_cast_type replace_var_by_pattern c) ) x and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) = if List.exists (fun id -> Id.compare id x_id == 0) idl @@ -541,11 +536,10 @@ let expand_as = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, - Miscops.map_cast_type (expand_as map) c) + Glob_ops.map_cast_type (expand_as map) c) | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) - | GProj(p,c) -> GProj(p, expand_as map c) ) and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} = CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt) @@ -563,7 +557,8 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect (* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed. If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *) let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in - let ctx, f = Evarutil.nf_evars_and_universes ctx in + let ctx = Evd.minimize_universes ctx in + let f c = EConstr.of_constr (Evarutil.nf_evars_universes ctx (EConstr.Unsafe.to_constr c)) in (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = @@ -575,7 +570,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (fun _ evi _ -> match evi.evar_source with | (loc_evi,ImplicitArg(gr_evi,p_evi,b_evi)) -> - if Globnames.eq_gr grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi + if GlobRef.equal grk gr_evi && pk=p_evi && bk=b_evi && rt.CAst.loc = loc_evi then raise (Found evi) | _ -> () ) @@ -586,8 +581,8 @@ If someone knows how to prevent solved existantial removal in understand, pleas with Found evi -> (* we found the evar corresponding to this hole *) match evi.evar_body with | Evar_defined c -> - (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + (* we just have to lift the solution in glob_term *) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -609,7 +604,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 7088ae596b..481a8be3ba 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -13,7 +13,7 @@ val pattern_to_term : cases_pattern -> glob_constr Some basic functions to rebuild glob_constr In each of them the location is Util.Loc.ghost *) -val mkGRef : Globnames.global_reference -> glob_constr +val mkGRef : GlobRef.t -> glob_constr val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9c350483b3..35acbea488 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -77,8 +77,7 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - let princ = EConstr.of_constr princ in - (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g') + (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)) -> @@ -91,10 +90,19 @@ let functional_induction with_clean c princl pat = 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,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) - (args@c_list) 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 = @@ -214,7 +222,6 @@ let is_rec names = | GCases(_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl - | GProj(_,c) -> lookup names c and lookup_br names {CAst.v=(idl,_,rt)} = let new_names = List.fold_right Id.Set.remove idl names in lookup new_names rt @@ -252,7 +259,6 @@ let derive_inversion fix_names = let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in evd, (cst, EInstance.kind evd u) :: l ) @@ -274,8 +280,7 @@ let derive_inversion fix_names = (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id))) in - let id = EConstr.of_constr id in - evd,(fst (destInd evd id))::l + evd,(fst (destInd evd id))::l ) fix_names (evd',[]) @@ -356,17 +361,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*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 = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in let ind_kn = fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + 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 @@ -379,7 +384,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let evd = ref (Evd.from_env env) in let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) 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 @@ -408,7 +414,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComDefinition.do_definition ~program_mode:false fname - (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl + (Decl_kinds.Global,false,Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left @@ -416,7 +422,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in - let c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -426,14 +431,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global false fixpoint_exprl; 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 c = EConstr.of_constr c in let (cst, u) = destConst evd c in let u = EInstance.kind evd u in evd,((cst, u) :: l) @@ -472,7 +476,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -482,7 +486,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + 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 @@ -539,9 +543,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - 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 @@ -722,12 +726,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof () let rec add_args id new_args = CAst.map (function - | CRef (r,_) as b -> - begin match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | 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) @@ -741,13 +743,10 @@ let rec add_args id new_args = CAst.map (function 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,r,us),exprl) -> - begin - match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) - end + | 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) @@ -777,13 +776,12 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + 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.") - | CProj _ -> user_err Pp.(str "Funind does not support primitive projections") ) exception Stop of Constrexpr.constr_expr @@ -842,7 +840,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph (f_ref:global_reference) = +let make_graph (f_ref : GlobRef.t) = let c,c_body = match f_ref with | ConstRef c -> @@ -883,7 +881,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) nal | Constrexpr.CLocalPattern _ -> assert false ) @@ -900,11 +898,11 @@ let make_graph (f_ref:global_reference) = let id = Label.to_id (Constant.label c) in [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in - let mp,dp,_ = Constant.repr3 c in + let mp = Constant.modpath c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index dcc1c2ea6a..f209fb19fd 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,4 +1,5 @@ -open Misctypes +open Names +open Tactypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit @@ -18,4 +19,4 @@ val functional_induction : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma -val make_graph : Globnames.global_reference -> unit +val make_graph : GlobRef.t -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a0b9217c75..c864bfe9f7 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -27,13 +27,7 @@ let array_get_start a = (Array.length a - 1) (fun i -> a.(i)) -let id_of_name = function - Name id -> id - | _ -> raise Not_found - -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with @@ -107,17 +101,9 @@ let const_of_id id = CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Id.print id) -let def_of_const t = - match Constr.kind t with - Term.Const sp -> - (try (match Environ.constant_opt_value_in (Global.env()) sp with - | Some c -> c - | _ -> assert false) - with Not_found -> assert false) - |_ -> assert false - +[@@@ocaml.warning "-3"] let coq_constant s = - Universes.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -161,17 +147,6 @@ let save with_clean id const (locality,_,kind) hook = CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id - - -let cook_proof _ = - let (id,(entry,_,strength)) = Pfedit.cook_proof () in - (id,(entry,strength)) - -let get_proof_clean do_reduce = - let result = cook_proof do_reduce in - Proof_global.discard_current (); - result - let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () @@ -269,12 +244,12 @@ let subst_Function (subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -299,36 +274,7 @@ let subst_Function (subst,finfos) = let classify_Function infos = Libobject.Substitute infos -let discharge_Function (_,finfos) = - let function_constant' = Lib.discharge_con finfos.function_constant - and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma - in - if function_constant' == finfos.function_constant && - graph_ind' == finfos.graph_ind && - equation_lemma' == finfos.equation_lemma && - correctness_lemma' == finfos.correctness_lemma && - completeness_lemma' == finfos.completeness_lemma && - rect_lemma' == finfos.rect_lemma && - rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma - then Some finfos - else - Some { function_constant = function_constant' ; - graph_ind = graph_ind' ; - equation_lemma = equation_lemma' ; - correctness_lemma = correctness_lemma' ; - completeness_lemma = completeness_lemma'; - rect_lemma = rect_lemma'; - rec_lemma = rec_lemma'; - prop_lemma = prop_lemma' ; - is_general = finfos.is_general - } +let discharge_Function (_,finfos) = Some finfos let pr_ocst c = let sigma, env = Pfedit.get_current_context () in @@ -341,7 +287,7 @@ let pr_info f_info = str "function_constant_type := " ++ (try Printer.pr_lconstr_env env sigma - (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant))) + (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant))) with e when CErrors.noncritical e -> mt ()) ++ fnl () ++ str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++ str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++ @@ -429,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig = optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) } -let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig +let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true @@ -442,7 +388,7 @@ let function_debug_sig = optwrite = (fun b -> function_debug := b) } -let _ = declare_bool_option function_debug_sig +let () = declare_bool_option function_debug_sig let do_observe () = !function_debug @@ -460,7 +406,7 @@ let strict_tcc_sig = optwrite = (fun b -> strict_tcc := b) } -let _ = declare_bool_option strict_tcc_sig +let () = declare_bool_option strict_tcc_sig exception Building_graph of exn @@ -471,16 +417,16 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq" + UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - Universes.constr_of_global @@ - Coqlib.coq_reference "Function" ["Logic";"JMeq"] "JMeq_refl" + UnivGen.constr_of_monomorphic_global @@ + Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = @@ -492,8 +438,10 @@ let well_founded = function () -> EConstr.of_constr (coq_constant "well_founded" let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") -let well_founded_ltof () = EConstr.of_constr @@ Universes.constr_of_global @@ - Coqlib.coq_reference "" ["Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "-3"] +let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + Coqlib.find_reference "IndFun" ["Coq"; "Arith";"Wf_nat"] "well_founded_ltof" +[@@@ocaml.warning "+3"] let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof") diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5cc7163aa3..c9d153d89f 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -18,13 +18,11 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t val array_get_start : 'a array -> 'a array -val id_of_name : Name.t -> Id.t - -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : @@ -38,24 +36,14 @@ val chop_rlambda_n : int -> Glob_term.glob_constr -> val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr -val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t -val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) +val const_of_id: Id.t -> GlobRef.t(* constantyes *) val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook CEphemeron.key -> unit - -(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and - abort the proof -*) -val get_proof_clean : bool -> - Names.Id.t * - (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) - - + Lemmas.declaration_hook CEphemeron.key -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. @@ -107,11 +95,11 @@ val h_intros: Names.Id.t list -> Tacmach.tactic val h_id : Names.Id.t val hrec_id : Names.Id.t val acc_inv_id : EConstr.constr Util.delayed -val ltof_ref : Globnames.global_reference Util.delayed +val ltof_ref : GlobRef.t Util.delayed val well_founded_ltof : EConstr.constr Util.delayed val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed -val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference +val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 2743a8a2f9..d1a227d517 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,7 +23,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Misctypes +open Tactypes open Termops open Context.Rel.Declaration @@ -63,12 +63,6 @@ let observe_tac s tac g = then do_observe_tac (str s) tac g else tac g -(* [nf_zeta] $\zeta$-normalization of a term *) -let nf_zeta = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - Environ.empty_env - Evd.empty - let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *) @@ -81,10 +75,9 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ())) - with _ -> assert false + EConstr.of_constr (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "core.eq.type")) + with _ -> assert false - (* [generate_type g_to_f f graph i] build the completeness (resp. correctness) lemma type if [g_to_f = true] (resp. g_to_f = false) where [graph] is the graph of [f] and is the [i]th function in the block. @@ -102,9 +95,9 @@ let generate_type evd g_to_f f graph i = let evd',graph = Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) in - let graph = EConstr.of_constr graph in evd:=evd'; - let graph_arity = Typing.e_type_of (Global.env ()) evd graph in + let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in + evd := sigma; let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with @@ -172,7 +165,6 @@ let find_induction_principle evd f = | None -> raise Not_found | Some rect_lemma -> let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in - let rect_lemma = EConstr.of_constr rect_lemma in let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in evd:=evd'; rect_lemma,typ @@ -221,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let mib,_ = Global.lookup_inductive graph_ind in (* and the principle to use in this lemma in $\zeta$ normal form *) let f_principle,princ_type = schemes.(i) in - let princ_type = nf_zeta princ_type in + let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in let princ_infos = Tactics.compute_elim_sig evd princ_type in (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in @@ -240,7 +232,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -258,7 +250,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.fold_right (fun {CAst.v=pat} acc -> match pat with - | IntroNaming (IntroIdentifier id) -> id::acc + | IntroNaming (Namegen.IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) @@ -352,7 +344,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i Locusops.onConcl); observe_tac ("toto ") tclIDTAC; - (* introducing the the result of the graph and the equality hypothesis *) + (* introducing the result of the graph and the equality hypothesis *) observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]); (* replacing [res] with its value *) observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres))); @@ -399,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in - (nf_zeta p)::bindings,id::avoid) + (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) @@ -451,7 +443,7 @@ let generalize_dependent_of x hyp g = let tauto = let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in let mp = ModPath.MPfile (DirPath.make dp) in - let kn = KerName.make2 mp (Label.make "tauto") in + let kn = KerName.make mp (Label.make "tauto") in Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> let body = Tacenv.interp_ltac kn in Tacinterp.eval_tactic body @@ -513,7 +505,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.False.type")) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENLIST[ @@ -632,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti *) let lemmas = Array.map - (fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt)) + (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt)) lemmas_types_infos in (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(i) in - let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in + let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i)) in let princ_type = pf_unsafe_type_of g graph_principle in let princ_infos = Tactics.compute_elim_sig (project g) princ_type in (* Then we get the number of argument of the function @@ -771,8 +763,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in graphs_constr.(i) <- graph; let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in - let type_of_lemma = nf_zeta type_of_lemma in + let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in + evd := sigma; + let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma); type_of_lemma,type_info ) @@ -811,20 +804,19 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem))) + (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem))) !evd typ (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *) let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with correctness_lemma = Some lem_cst}; ) @@ -840,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in - let type_of_lemma = nf_zeta type_of_lemma in + let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma); type_of_lemma,type_info ) @@ -874,18 +866,17 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list i*) let lem_id = mk_complete_id f_id in Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma (fst lemmas_types_infos.(i)) (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)))); + (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); let finfo = find_Function_infos (fst f_as_constant) in let _,lem_cst_constr = Evd.fresh_global (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in - let lem_cst_constr = EConstr.of_constr lem_cst_constr in - let (lem_cst,_) = destConst !evd lem_cst_constr in + let (lem_cst,_) = destConst !evd lem_cst_constr in update_Function {finfo with completeness_lemma = Some lem_cst} ) funs) @@ -969,7 +960,7 @@ let functional_inversion kn hid fconst f_correct : Tacmach.tactic = Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); - Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); + Proofview.V82.of_tactic (Inv.inv Inv.FullInversion None (NamedHyp hid)); (fun g -> let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in tclMAP (revert_graph kn pre_tac) (hid::new_ids) g diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index ad306ab257..3ddc609201 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -9,8 +9,8 @@ (************************************************************************) val invfun : - Misctypes.quantified_hypothesis -> - Globnames.global_reference option -> + Tactypes.quantified_hypothesis -> + Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : (Evd.evar_map ref -> diff --git a/plugins/funind/plugin_base.dune b/plugins/funind/plugin_base.dune new file mode 100644 index 0000000000..002eb28eea --- /dev/null +++ b/plugins/funind/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name recdef_plugin) + (public_name coq.plugins.recdef) + (synopsis "Coq's functional induction plugin") + (libraries coq.plugins.extraction)) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fb9ae64bf4..6e5e3f9353 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -24,6 +24,7 @@ open Globnames open Nameops open CErrors open Util +open UnivGen open Tacticals open Tacmach open Tactics @@ -37,7 +38,7 @@ open Glob_term open Pretyping open Termops open Constrintern -open Misctypes +open Tactypes open Genredexpr open Equality @@ -49,11 +50,12 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) -let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ - Coqlib.coq_reference "RecursiveDefinition" m s +[@@@ocaml.warning "-3"] +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ + Coqlib.find_reference "RecursiveDefinition" m s -let arith_Nat = ["Arith";"PeanoNat";"Nat"] -let arith_Lt = ["Arith";"Lt"] +let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"] +let arith_Lt = ["Coq"; "Arith";"Lt"] let pr_leconstr_rd = let sigma, env = Pfedit.get_current_context () in @@ -61,8 +63,9 @@ let pr_leconstr_rd = let coq_init_constant s = EConstr.of_constr ( - Universes.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) +[@@@ocaml.warning "+3"] let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -72,7 +75,7 @@ let declare_fun f_id kind ?univs value = let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None))) let def_of_const t = match (Constr.kind t) with @@ -94,30 +97,12 @@ let type_of_const sigma t = Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false -let constr_of_global x = - fst (Global.constr_of_global_in_context (Global.env ()) x) - -let constant sl s = constr_of_global (find_reference sl s) +let constant sl s = UnivGen.constr_of_monomorphic_global (find_reference sl s) let const_of_ref = function ConstRef kn -> kn | _ -> anomaly (Pp.str "ConstRef expected.") - -let nf_zeta env = - Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) - env - Evd.empty - - -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty - - - - - - (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in @@ -143,6 +128,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") +[@@@ocaml.warning "-3"] let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") @@ -163,7 +149,6 @@ let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) -let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -181,7 +166,7 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f: Constr.t list -> global_reference -> Constr.t) = +let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = let open Term in let open Constr in fun al fterm -> @@ -215,7 +200,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) = let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -356,7 +341,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functional reference *) + func : GlobRef.t; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -713,7 +698,7 @@ let mkDestructEq : observe_tclTHENLIST (str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> - let changefun patvars sigma = + let changefun patvars env sigma = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in Proofview.V82.of_tactic (change_in_concl None changefun) g2); @@ -747,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = with | UserError(Some "Refiner.thensn_tac3",_) | UserError(Some "Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) )) g @@ -1152,7 +1137,7 @@ let termination_proof_header is_mes input_type ids args_id relation tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1))); + observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); h_intros args_id; Proofview.V82.of_tactic (Simple.intro wf_rec_arg); observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) @@ -1241,8 +1226,8 @@ let get_current_subgoals_types () = exception EmptySubgoals let build_and_l sigma l = - let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in - let conj_constr = coq_conj () in + let and_constr = UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.and.type" in + let conj_constr = Coqlib.build_coq_conj () in let mk_and p1 p2 = mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = @@ -1306,9 +1291,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque - | Declarations.Undef _ -> Vernacexpr.Opaque - | Declarations.Def _ -> Vernacexpr.Transparent + | Declarations.OpaqueDef _ -> Proof_global.Opaque + | Declarations.Undef _ -> Proof_global.Opaque + | Declarations.Def _ -> Proof_global.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) @@ -1318,14 +1303,14 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | None -> try add_suffix current_proof_name "_subproof" with e when CErrors.noncritical e -> - anomaly (Pp.str "open_new_goal with an unamed theorem.") + anomaly (Pp.str "open_new_goal with an unnamed theorem.") in let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1374,7 +1359,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Eauto.eauto_with_bases (true,5) [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] - [Hints.Hint_db.empty empty_transparent_state false] + [Hints.Hint_db.empty TransparentState.empty false] ] ) ) @@ -1456,7 +1441,7 @@ let com_terminate -let start_equation (f:global_reference) (term_f:global_reference) +let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = let sigma = project g in let ids = pf_ids_of_hyps g in @@ -1473,7 +1458,7 @@ let start_equation (f:global_reference) (term_f:global_reference) observe_tac (str "prove_eq") (cont_tactic x)]) g;; let (com_eqn : int -> Id.t -> - global_reference -> global_reference -> global_reference + GlobRef.t -> GlobRef.t -> GlobRef.t -> Constr.t -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in @@ -1533,19 +1518,17 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let env = Global.env() in let evd = Evd.from_env env in let evd, function_type = interp_type_evars env evd type_of_f in - let function_type = EConstr.Unsafe.to_constr function_type in - let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in - let ty = EConstr.Unsafe.to_constr ty in - let evd, nf = Evarutil.nf_evars_and_universes evd in - let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in - let function_type = nf function_type in + let evd = Evd.minimize_universes evd in + let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in + let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in - let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in + let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in let eq' = EConstr.Unsafe.to_constr eq' in let res = (* Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) @@ -1579,7 +1562,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index b95d64ce9e..549f1fc0e4 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -14,6 +14,6 @@ bool -> int -> Constrexpr.constr_expr -> (pconstant -> Indfun_common.tcc_lemma_value ref -> pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> 'a) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> unit |