diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/g_indfun.mlg | 47 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 36 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 13 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 24 |
5 files changed, 83 insertions, 43 deletions
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index bdd30aae0a..833ff9f1ed 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -173,24 +173,41 @@ let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer +let is_proof_termination_interactively_checked recsl = + List.exists (function + | _,((_,( Some { CAst.v = CMeasureRec _ } + | Some { CAst.v = CWfRec _}),_,_,_),_) -> true + | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) + | _,((_,None,_,_,_),_) -> false) recsl + +let classify_as_Fixpoint recsl = + Vernac_classifier.classify_vernac + (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) + +let classify_funind recsl = + match classify_as_Fixpoint recsl with + | Vernacextend.VtSideff ids, _ + when is_proof_termination_interactively_checked recsl -> + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) + | x -> x + +let is_interactive recsl = + match classify_funind recsl with + | Vernacextend.VtStartProof _, _ -> true + | _ -> false + } -(* TASSI: n'importe quoi ! *) -VERNAC COMMAND EXTEND Function STATE maybe_open_proof +VERNAC COMMAND EXTEND Function STATE CUSTOM | ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => { let hard = List.exists (function - | _,((_,(Some { CAst.v = CMeasureRec _ } - | Some { CAst.v = CWfRec _}),_,_,_),_) -> true - | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_) - | _,((_,None,_,_,_),_) -> false) recsl in - match - Vernac_classifier.classify_vernac - (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) - with - | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) - | x -> x } - -> { do_generate_principle false (List.map snd recsl) } + => { classify_funind recsl } + -> { + if is_interactive recsl then + Vernacextend.VtOpenProof (fun () -> + do_generate_principle_interactive (List.map snd recsl)) + else + Vernacextend.VtDefault (fun () -> + do_generate_principle (List.map snd recsl)) } END { diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7c6669d0fc..bb6db1f5cf 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -459,7 +459,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation -let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body +let register_wf interactive_proof ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = let type_of_f = Constrexpr_ops.mkCProdN args ret_type in @@ -500,8 +500,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas (* No proof done *) () in - Recdef.recursive_definition - is_mes fname rec_impls + Recdef.recursive_definition ~interactive_proof + ~is_mes fname rec_impls type_of_f wf_rel_expr rec_arg_num @@ -510,7 +510,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas using_lemmas -let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = +let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas args ret_type body = let wf_arg_type,wf_arg = match wf_arg with | None -> @@ -570,7 +570,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas in wf_rel_with_mes,false in - register_wf ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg + register_wf interactive_proof ~is_mes:is_mes fname rec_impls wf_rel_from_mes wf_arg using_lemmas args ret_type body let map_option f = function @@ -633,7 +633,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex fixpoint_exprl_with_new_bl -let do_generate_principle pconstants on_error register_built interactive_proof +let do_generate_principle_aux pconstants on_error register_built interactive_proof (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; let pstate, _is_struct = @@ -660,7 +660,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false + then register_wf interactive_proof name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false else None, false |[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = @@ -684,7 +684,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true + then register_mes interactive_proof name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true else None, true | _ -> List.iter (function ((_na,ord,_args,_body,_type),_not) -> @@ -902,11 +902,27 @@ let make_graph (f_ref : GlobRef.t) = [((CAst.make id,None),None,nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in + let pstate = do_generate_principle_aux [c,Univ.Instance.empty] error_error false false expr_list in assert (Option.is_empty pstate); (* We register the infos *) List.iter (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 +(* *************** statically typed entrypoints ************************* *) + +let do_generate_principle_interactive fixl : Proof_global.t = + match + do_generate_principle_aux [] warning_error true true fixl + with + | Some pstate -> pstate + | None -> + CErrors.anomaly + (Pp.str"indfun: leaving no open proof in interactive mode") + +let do_generate_principle fixl : unit = + match do_generate_principle_aux [] warning_error true false fixl with + | Some _pstate -> + CErrors.anomaly + (Pp.str"indfun: leaving a goal open in non-interactive mode") + | None -> () diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 47d37b29a5..1ba245a45d 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -6,9 +6,11 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : - bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +val do_generate_principle_interactive : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - Proof_global.t option + Proof_global.t val functional_induction : bool -> diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5a682e7231..e2321d233c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1395,12 +1395,10 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type ) tclIDTAC) g end) pstate in - try - Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) - with UserError _ -> - (defined pstate; None) + if Proof_global.get_open_goals pstate = 0 then (defined pstate; None) else Some pstate let com_terminate + interactive_proof tcc_lemma_name tcc_lemma_ref is_mes @@ -1430,8 +1428,8 @@ let com_terminate with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined pstate; - None + if interactive_proof then Some pstate + else (defined pstate; None) let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1494,7 +1492,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation (* Pp.msgnl (fun _ _ -> str "eqn finished"); *) -let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq +let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type_of_f r rec_arg_num eq generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in @@ -1585,6 +1583,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num (* XXX STATE Why do we need this... why is the toplevel protection not enough *) funind_purify (fun () -> let pstate = com_terminate + interactive_proof tcc_lemma_name tcc_lemma_constr is_mes functional_ref diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 90f9c449b1..b92ac3a0ec 100644 --- a/plugins/funind/recdef.mli +++ b/plugins/funind/recdef.mli @@ -5,13 +5,19 @@ val tclUSER_if_not_mes : bool -> Names.Id.t list option -> Tacmach.tactic + val recursive_definition : -bool -> - Names.Id.t -> - Constrintern.internalization_env -> - Constrexpr.constr_expr -> - Constrexpr.constr_expr -> - int -> Constrexpr.constr_expr -> (pconstant -> - Indfun_common.tcc_lemma_value ref -> - pconstant -> - pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option + interactive_proof:bool -> + is_mes:bool -> + Names.Id.t -> + Constrintern.internalization_env -> + Constrexpr.constr_expr -> + Constrexpr.constr_expr -> + int -> + Constrexpr.constr_expr -> + (pconstant -> + Indfun_common.tcc_lemma_value ref -> + pconstant -> + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> + Constrexpr.constr_expr list -> + Proof_global.t option |