diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 45 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 117 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 24 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 19 |
4 files changed, 100 insertions, 105 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 7b2ce671a3..b864b18887 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -41,7 +41,10 @@ let observe_tac s = observe_tac (fun _ _ -> Pp.str s) let finish_proof dynamic_infos g = observe_tac "finish" (Proofview.V82.of_tactic assumption) g -let refine c = Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c) +let refine c = + Proofview.V82.of_tactic + (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr c)) + let thin l = Proofview.V82.of_tactic (Tactics.clear l) let eq_constr sigma u v = EConstr.eq_constr_nounivs sigma u v @@ -113,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) = refine to_refine g) ] let find_rectype env sigma c = - let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in + let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in match EConstr.kind sigma t with | Ind ind -> (t, l) | Construct _ -> (t, l) @@ -240,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type = let new_ctxt, new_end_of_type = decompose_prod_n_assum sigma ctxt_size new_type_of_hyp in - let prove_new_hyp : tactic = - tclTHEN - (tclDO ctxt_size (Proofview.V82.of_tactic intro)) - (fun g -> - let all_ids = pf_ids_of_hyps g in - let new_ids, _ = list_chop ctxt_size all_ids in - let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in - let evm, _ = pf_apply Typing.type_of g to_refine in - tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g) + let prove_new_hyp = + let open Tacticals.New in + let open Tacmach.New in + tclTHEN (tclDO ctxt_size intro) + (Proofview.Goal.enter (fun g -> + let all_ids = pf_ids_of_hyps g in + let new_ids, _ = list_chop ctxt_size all_ids in + let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in + let evm, _ = + Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g) + to_refine + in + tclTHEN + (Proofview.Unsafe.tclEVARS evm) + (Proofview.V82.tactic (refine to_refine)))) in let simpl_eq_tac = change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp - prove_new_hyp + (Proofview.V82.of_tactic prove_new_hyp) in (* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *) (* str "removing an equation " ++ fnl ()++ *) @@ -531,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id = let prov_hid = pf_get_new_id hid g in let c = mkApp (mkVar hid, args) in let evm, _ = pf_apply Typing.type_of g c in - tclTHENLIST - [ Refiner.tclEVARS evm - ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c) - ; thin [hid] - ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ] + let open Tacticals.New in + Proofview.V82.of_tactic + (tclTHENLIST + [ Proofview.Unsafe.tclEVARS evm + ; pose_proof (Name prov_hid) c + ; clear [hid] + ; rename_hyp [(prov_hid, hid)] ]) g) (fun (* if not then we are in a mutual function block diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 55e659d487..608155eb71 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -159,7 +159,7 @@ let recompute_binder_list fixpoint_exprl = fixpoint_exprl in let (_, _, _, typel), _, ctx, _ = - ComFixpoint.interp_fixpoint ~cofix:false fixl + ComFixpoint.interp_fixpoint ~check_recursivity:false ~cofix:false fixl in let constr_expr_typel = with_full_print @@ -191,61 +191,35 @@ let prepare_body {Vernacexpr.binders} rt = let fun_args, rt' = chop_rlambda_n n rt in (fun_args, rt') -let build_functional_principle ?(opaque = Declare.Transparent) - (evd : Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook = +let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs + _i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = - (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)) + (Tactics.compute_elim_sig sigma (EConstr.of_constr old_princ_type)) .Tactics.nparams in - (* let time1 = System.get_time () in *) let new_principle_type = Functional_principles_types.compute_new_princ_type_from_rel (Array.map Constr.mkConstU funs) sorts old_princ_type in - (* let time2 = System.get_time () in *) - (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) - let new_princ_name = - Namegen.next_ident_away_in_goal - (Id.of_string "___________princ_________") - Id.Set.empty - in let sigma, _ = - Typing.type_of ~refresh:true (Global.env ()) !evd + Typing.type_of ~refresh:true (Global.env ()) sigma (EConstr.of_constr new_principle_type) in - evd := sigma; - let hook = DeclareDef.Hook.make (hook new_principle_type) in - let lemma = - Lemmas.start_lemma ~name:new_princ_name ~poly:false !evd - (EConstr.of_constr new_principle_type) - in - (* let _tim1 = System.get_time () in *) let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - let lemma, _ = - Lemmas.by - (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) - lemma + let ftac = + Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams) in - (* let _tim2 = System.get_time () in *) - (* begin *) - (* let dur1 = System.time_difference tim1 tim2 in *) - (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) - (* end; *) - let {Declare.entries} = - Lemmas.pf_fold - (Declare.close_proof ~opaque ~keep_body_ucst_separate:false) - lemma + let env = Global.env () in + let uctx = Evd.evar_universe_context sigma in + let typ = EConstr.of_constr new_principle_type in + let body, typ, univs, _safe, _uctx = + Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac in - match entries with - | [entry] -> (entry, hook) - | _ -> - CErrors.anomaly - Pp.( - str - "[build_functional_principle] close_proof returned more than one \ - proof term") + (* uctx was ignored before *) + let hook = Declare.Hook.make (hook new_principle_type) in + (body, typ, univs, hook, sigma) let change_property_sort evd toSort princ princName = let open Context.Rel.Declaration in @@ -333,17 +307,19 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts register_with_sort Sorts.InProp; register_with_sort Sorts.InSet ) in - let entry, hook = - build_functional_principle evd old_princ_type new_sorts funs i proof_tac + let body, types, univs, hook, sigma0 = + build_functional_principle !evd old_princ_type new_sorts funs i proof_tac hook in + evd := sigma0; (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) let uctx = Evd.evar_universe_context sigma in + let entry = Declare.definition_entry ~univs ?types body in let (_ : Names.GlobRef.t) = - DeclareDef.declare_entry ~name:new_princ_name ~hook - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + Declare.declare_entry ~name:new_princ_name ~hook + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.(IsProof Theorem) ~impargs:[] ~uctx entry in @@ -424,7 +400,7 @@ let register_struct is_rec fixpoint_exprl = Pp.(str "Body of Function must be given") in ComDefinition.do_definition ~name:fname.CAst.v ~poly:false - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~kind:Decls.Definition univs binders None body (Some rtype); let evd, rev_pconstants = List.fold_left @@ -443,7 +419,7 @@ let register_struct is_rec fixpoint_exprl = (None, evd, List.rev rev_pconstants) | _ -> ComFixpoint.do_fixpoint - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false + ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl; let evd, rev_pconstants = List.fold_left @@ -1334,8 +1310,7 @@ let get_funs_constant mp = in l_const -let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : - Evd.side_effects Declare.proof_entry list = +let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let exception Found_type of int in let env = Global.env () in let funs = List.map fst fas in @@ -1402,18 +1377,19 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent in - let entry, _hook = + let body, typ, univs, _hook, sigma0 = try - build_functional_principle ~opaque evd first_type (Array.of_list sorts) + build_functional_principle !evd first_type (Array.of_list sorts) this_block_funs 0 (Functional_principles_proofs.prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) (fun _ _ -> ()) with e when CErrors.noncritical e -> raise (Defining_principle e) in + evd := sigma0; incr i; (* The others are just deduced *) - if List.is_empty other_princ_types then [entry] + if List.is_empty other_princ_types then [(body, typ, univs, opaque)] else let other_fun_princ_types = let funs = Array.map Constr.mkConstU this_block_funs in @@ -1422,10 +1398,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body = entry.Declare.proof_entry_body in - let ctxt, fix = - Term.decompose_lam_assum (fst (fst (Future.force first_princ_body))) - in + let first_princ_body = body in + let ctxt, fix = Term.decompose_lam_assum first_princ_body in (* the principle has for forall ...., fix .*) let (idxs, _), ((_, ta, _) as decl) = Constr.destFix fix in let other_result = @@ -1457,8 +1431,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let entry, _hook = - build_functional_principle evd + let body, typ, univs, _hook, sigma0 = + build_functional_principle !evd (List.nth other_princ_types (!i - 1)) (Array.of_list sorts) this_block_funs !i (Functional_principles_proofs.prove_princ_for_struct evd false @@ -1466,15 +1440,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : (Array.of_list (List.map fst funs))) (fun _ _ -> ()) in - entry + evd := sigma0; + (body, typ, univs, opaque) with Found_type i -> let princ_body = Termops.it_mkLambda_or_LetIn (Constr.mkFix ((idxs, i), decl)) ctxt in - Declare.definition_entry ~types:scheme_type princ_body) + (princ_body, Some scheme_type, univs, opaque)) other_fun_princ_types in - entry :: other_result + (body, typ, univs, opaque) :: other_result (* [derive_correctness funs graphs] create correctness and completeness lemmas for each function in [funs] w.r.t. [graphs] @@ -1527,11 +1502,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) with Not_found -> Array.of_list (List.map - (fun entry -> - ( EConstr.of_constr - (fst (fst (Future.force entry.Declare.proof_entry_body))) - , EConstr.of_constr (Option.get entry.Declare.proof_entry_type) - )) + (fun (body, typ, _opaque, _univs) -> + (EConstr.of_constr body, EConstr.of_constr (Option.get typ))) (make_scheme evd (Array.map_to_list (fun const -> (const, Sorts.InType)) funs))) in @@ -2225,11 +2197,14 @@ let build_scheme fas = in let bodies_types = make_scheme evd pconstants in List.iter2 - (fun (princ_id, _, _) def_entry -> - ignore - (Declare.declare_constant ~name:princ_id - ~kind:Decls.(IsProof Theorem) - (Declare.DefinitionEntry def_entry)); + (fun (princ_id, _, _) (body, types, univs, opaque) -> + let (_ : Constant.t) = + let opaque = if opaque = Declare.Opaque then true else false in + let def_entry = Declare.definition_entry ~univs ~opaque ?types body in + Declare.declare_constant ~name:princ_id + ~kind:Decls.(IsProof Theorem) + (Declare.DefinitionEntry def_entry) + in Declare.definition_message princ_id) fas bodies_types diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index e83fe56cc9..af53f16e1f 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -2,7 +2,7 @@ open Names open Pp open Constr open Libnames -open Refiner +open Tacmach let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id) let mk_rel_id = mk_prefix "R_" @@ -395,7 +395,8 @@ let jmeq_refl () = with e when CErrors.noncritical e -> raise (ToShow e) let h_intros l = - tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l + Proofview.V82.of_tactic + (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l) let h_id = Id.of_string "h" let hrec_id = Id.of_string "hrec" @@ -427,15 +428,16 @@ let evaluable_of_global_reference r = | _ -> assert false let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) = - tclREPEAT - (List.fold_right - (fun (eq, b) i -> - tclORELSE - (Proofview.V82.of_tactic - ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) - i) - (if rev then List.rev eqs else eqs) - (tclFAIL 0 (mt ()))) + let open Tacticals in + (tclREPEAT + (List.fold_right + (fun (eq, b) i -> + tclORELSE + (Proofview.V82.of_tactic + ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) + i) + (if rev then List.rev eqs else eqs) + (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"]) let decompose_lam_n sigma n = if n < 0 then diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ffb9a7e69b..9b2d9c4815 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g = in continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g -let pf_type c tac gl = - let evars, ty = Typing.type_of (pf_env gl) (project gl) c in - tclTHEN (Refiner.tclEVARS evars) (tac ty) gl +let pf_type c tac = + let open Tacticals.New in + Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let evars, ty = Typing.type_of env sigma c in + tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty)) + +let pf_type c tac = + Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty))) let pf_typel l tac = let rec aux tys l = @@ -1483,7 +1490,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in + let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type in @@ -1721,7 +1728,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook {DeclareDef.Hook.S.uctx; _} = + let hook {Declare.Hook.S.uctx; _} = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref @@ -1767,5 +1774,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls functional_ref (EConstr.of_constr rec_arg_type) relation rec_arg_num term_id using_lemmas (List.length res_vars) evd - (DeclareDef.Hook.make hook)) + (Declare.Hook.make hook)) () |