diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 155 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 157 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.mlg (renamed from plugins/funind/g_indfun.ml4) | 187 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 150 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 73 | ||||
| -rw-r--r-- | plugins/funind/indfun.mli | 14 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 97 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 35 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 87 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 460 | ||||
| -rw-r--r-- | plugins/funind/recdef.mli | 2 |
12 files changed, 681 insertions, 742 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b12364d04a..287a374ab1 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -2,6 +2,7 @@ open Printer open CErrors open Util open Constr +open Context open EConstr open Vars open Namegen @@ -44,10 +45,6 @@ let observe_tac s tac g = observe_tac_stream (str s) tac g *) -let pr_leconstr_fp = - let sigma, env = Pfedit.get_current_context () in - Printer.pr_leconstr_env env sigma - let debug_queue = Stack.create () let rec print_debug_queue e = @@ -131,8 +128,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) @@ -164,7 +160,7 @@ let rec incompatible_constructor_terms sigma t1 t2 = List.exists2 (incompatible_constructor_terms sigma) arg1 arg2 ) -let is_incompatible_eq sigma t = +let is_incompatible_eq env sigma t = let res = try match EConstr.kind sigma t with @@ -176,7 +172,7 @@ let is_incompatible_eq sigma t = | _ -> false with e when CErrors.noncritical e -> false in - if res then observe (str "is_incompatible_eq " ++ pr_leconstr_fp t); + if res then observe (str "is_incompatible_eq " ++ pr_leconstr_env env sigma t); res let change_hyp_with_using msg hyp_id t tac : tactic = @@ -229,10 +225,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.from_env Environ.empty_env - - exception NoChange let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = @@ -243,7 +235,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false 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"; @@ -305,7 +299,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = in let old_context_length = List.length context + 1 in let witness_fun = - mkLetIn(Anonymous,make_refl_eq constructor t1_typ (fst t1),t, + mkLetIn(make_annot Anonymous Sorts.Relevant,make_refl_eq constructor t1_typ (fst t1),t, mkApp(mkVar hyp_id,Array.init old_context_length (fun i -> mkRel (old_context_length - i))) ) in @@ -315,7 +309,8 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = try let witness = Int.Map.find i sub in if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); - (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_name decl, witness, RelDecl.get_type decl, witness_fun)) + (pop end_of_type,ctxt_size,mkLetIn (RelDecl.get_annot decl, + witness, RelDecl.get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -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 (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type") in - let coq_True = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.type") in - let coq_I = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.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 @@ -431,7 +426,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = else if isProd sigma type_of_hyp then begin - let (x,t_x,t') = destProd sigma type_of_hyp in + let (x,t_x,t') = destProd sigma type_of_hyp in let actual_real_type_of_hyp = it_mkProd_or_LetIn t' context in if is_property sigma ptes_infos t_x actual_real_type_of_hyp then begin @@ -481,7 +476,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (* ); *) raise TOREMOVE; (* False -> .. useless *) end - else if is_incompatible_eq sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) + else if is_incompatible_eq env sigma t_x then raise TOREMOVE (* t_x := C1 ... = C2 ... *) else if eq_constr sigma t_x coq_True (* Trivial => we remove this precons *) then (* observe (str "In "++Ppconstr.pr_id hyp_id++ *) @@ -544,7 +539,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with NoChange -> (* Last thing todo : push the rel in the context and continue *) - scan_type (LocalAssum (x,t_x) :: context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -613,7 +608,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = anomaly (Pp.str "cannot compute new term value.") in let fun_body = - mkLambda(Anonymous, + mkLambda(make_annot Anonymous Sorts.Relevant, pf_unsafe_type_of g' term, Termops.replace_term (project g') term (mkRel 1) dyn_infos.info ) @@ -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,12 +717,12 @@ 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 - (build_proof do_finalize) + nb_instantiate_partial + (build_proof do_finalize) t dyn_infos) g' @@ -738,8 +733,8 @@ let build_proof ] g in - build_proof do_finalize_t {dyn_infos with info = t} g - | Lambda(n,t,b) -> + build_proof do_finalize_t {dyn_infos with info = t} g + | Lambda(n,t,b) -> begin match EConstr.kind sigma (pf_concl g) with | Prod _ -> @@ -754,26 +749,27 @@ let build_proof in let new_infos = {dyn_infos with info = new_term} in let do_prove new_hyps = - build_proof do_finalize + build_proof do_finalize {new_infos with rec_hyps = new_hyps; 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 | _ -> do_finalize dyn_infos g end | Cast(t,_,_) -> - build_proof do_finalize {dyn_infos with info = t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + build_proof do_finalize {dyn_infos with info = t} g + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> do_finalize dyn_infos g | App(_,_) -> let f,args = decompose_app sigma dyn_infos.info in begin match EConstr.kind sigma f with + | Int _ -> user_err Pp.(str "integer cannot be applied") | App _ -> assert false (* we have collected all the app in decompose_app *) | Proj _ -> assert false (*FIXME*) | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ -> @@ -782,7 +778,7 @@ let build_proof info = (f,args) } in - build_proof_args do_finalize new_infos g + build_proof_args env sigma do_finalize new_infos g | Const (c,_) when not (List.mem_f Constant.equal c fnames) -> let new_infos = { dyn_infos with @@ -790,17 +786,17 @@ let build_proof } in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) - build_proof_args do_finalize new_infos g + build_proof_args env sigma do_finalize new_infos g | Const _ -> do_finalize dyn_infos g | Lambda _ -> let new_term = Reductionops.nf_beta env sigma dyn_infos.info in - build_proof do_finalize {dyn_infos with info = new_term} + build_proof do_finalize {dyn_infos with info = new_term} 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 @@ -809,11 +805,11 @@ let build_proof h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof do_finalize new_infos + build_proof do_finalize new_infos ] g | Cast(b,_,_) -> - build_proof do_finalize {dyn_infos with info = b } g + build_proof do_finalize {dyn_infos with info = b } g | Case _ | Fix _ | CoFix _ -> let new_finalize dyn_infos = let new_infos = @@ -821,9 +817,9 @@ let build_proof info = dyn_infos.info,args } in - build_proof_args do_finalize new_infos + build_proof_args env sigma do_finalize new_infos in - build_proof new_finalize {dyn_infos with info = f } g + build_proof new_finalize {dyn_infos with info = f } g end | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) @@ -834,7 +830,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 @@ -843,13 +839,13 @@ let build_proof (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) dyn_infos.rec_hyps; h_reduce_with_zeta Locusops.onConcl; - build_proof do_finalize new_infos + build_proof do_finalize new_infos ] g | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") and build_proof do_finalize dyn_infos g = (* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *) - observe_tac_stream (str "build_proof with " ++ pr_leconstr_fp dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g - and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic = + observe_tac_stream (str "build_proof with " ++ pr_leconstr_env (pf_env g) (project g) dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g + and build_proof_args env sigma do_finalize dyn_infos (* f_args' args *) :tactic = fun g -> let (f_args',args) = dyn_infos.info in let tac : tactic = @@ -865,12 +861,12 @@ let build_proof let do_finalize dyn_infos = let new_arg = dyn_infos.info in (* tclTRYD *) - (build_proof_args + (build_proof_args env sigma do_finalize {dyn_infos with info = (mkApp(f_args',[|new_arg|])), args} ) in - build_proof do_finalize + build_proof do_finalize {dyn_infos with info = arg } g in @@ -882,17 +878,8 @@ let build_proof finish_proof dyn_infos) in (* observe_tac "build_proof" *) - (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos) - - - - - - - - - - + fun g -> + build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos g (* Proof of principles from structural functions *) @@ -977,7 +964,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 @@ -1003,20 +990,18 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - Lemmas.start_proof + let pstate = Lemmas.start_proof ~ontop:None (*i The next call to mk_equation_id is valid since we are constructing the lemma 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(Proof_global.Transparent,None))); - evd - - + in + let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in + let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in + pstate, evd let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g = @@ -1030,7 +1015,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a Ensures by: obvious i*) let equation_lemma_id = (mk_equation_id f_id) in - evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; + evd := snd @@ generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with | Option.IsNone -> @@ -1120,7 +1105,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 ) @@ -1130,7 +1115,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 ) @@ -1152,7 +1137,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let fix_offset = List.length princ_params in let ptes_to_fix,infos = match EConstr.kind (project g) fbody_with_full_params with - | Fix((idxs,i),(names,typess,bodies)) -> + | Fix((idxs,i),(names,typess,bodies)) -> let bodies_with_all_params = Array.map (fun body -> @@ -1167,7 +1152,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.Name.get_id (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i).binder_name); types = types; offset = fix_offset; nb_realargs = @@ -1198,9 +1183,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam applist(body,List.rev_map var_of_decl full_params)) in match EConstr.kind (project g) body_with_full_params with - | Fix((_,num),(_,_,bs)) -> + | Fix((_,num),(_,_,bs)) -> Reductionops.nf_betaiota (pf_env g) (project g) - ( + ( (applist (substl (List.rev @@ -1321,7 +1306,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)) ] @@ -1371,7 +1356,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) ] @@ -1491,7 +1476,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] ) ) ) @@ -1517,7 +1502,7 @@ let is_valid_hypothesis sigma predicates_name = let rec is_valid_hypothesis typ = is_pte typ || match EConstr.kind sigma typ with - | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' + | Prod(_,pte,typ') -> is_pte pte && is_valid_hypothesis typ' | _ -> false in is_valid_hypothesis @@ -1568,7 +1553,7 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id + | (LocalAssum ({binder_name=Name id},_) | LocalDef ({binder_name=Name id},_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) @@ -1605,7 +1590,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 (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.True.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 *) @@ -1728,8 +1713,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 9ca91d62da..e9a2c285d0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -14,6 +14,7 @@ open Term open Sorts open Util open Constr +open Context open Vars open Namegen open Names @@ -41,7 +42,7 @@ let pop t = Vars.lift (-1) t *) let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let princ_type = EConstr.of_constr princ_type in - let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in + let princ_type_info = compute_elim_sig Evd.empty princ_type (* FIXME *) in let env = Global.env () in let env_with_params = EConstr.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in @@ -72,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (map_annot Nameops.Name.get_id (Context.Rel.Declaration.get_annot decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -137,14 +138,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Rel n -> begin try match Environ.lookup_rel n env with - | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved + | LocalAssum (_,t) | LocalDef (_,_,t) when is_dom t -> raise Toberemoved | _ -> pre_princ,[] with Not_found -> assert false end - | Prod(x,t,b) -> - compute_new_princ_type_for_binder remove mkProd env x t b - | Lambda(x,t,b) -> - compute_new_princ_type_for_binder remove mkLambda env x t b + | Prod(x,t,b) -> + compute_new_princ_type_for_binder remove mkProd env x t b + | Lambda(x,t,b) -> + compute_new_princ_type_for_binder remove mkLambda env x t b | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved | App(f,args) when is_dom f -> let var_to_be_removed = destRel (Array.last args) in @@ -164,8 +165,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in applistc new_f new_args, list_union_eq Constr.equal binders_to_remove_from_f binders_to_remove - | LetIn(x,v,t,b) -> - compute_new_princ_type_for_letin remove env x v t b + | LetIn(x,v,t,b) -> + compute_new_princ_type_for_letin remove env x v t b | _ -> pre_princ,[] in (* let _ = match Constr.kind pre_princ with *) @@ -181,14 +182,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = begin try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in - let new_x : Name.t = get_name (Termops.ids_of_context env) x in - let new_env = Environ.push_rel (LocalAssum (x,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x in + let new_env = Environ.push_rel (LocalAssum (x,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b), filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - bind_fun(new_x,new_t,new_b), + bind_fun(new_x,new_t,new_b), list_union_eq Constr.equal binders_to_remove_from_t @@ -210,14 +211,14 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = try let new_t,binders_to_remove_from_t = compute_new_princ_type remove env t in let new_v,binders_to_remove_from_v = compute_new_princ_type remove env v in - let new_x : Name.t = get_name (Termops.ids_of_context env) x in - let new_env = Environ.push_rel (LocalDef (x,v,t)) env in + let new_x = map_annot (get_name (Termops.ids_of_context env)) x in + let new_env = Environ.push_rel (LocalDef (x,v,t)) env in let new_b,binders_to_remove_from_b = compute_new_princ_type remove new_env b in if List.exists (Constr.equal (mkRel 1)) binders_to_remove_from_b then (pop new_b),filter_map (Constr.equal (mkRel 1)) pop binders_to_remove_from_b else ( - mkLetIn(new_x,new_v,new_t,new_b), + mkLetIn(new_x,new_v,new_t,new_b), list_union_eq Constr.equal (list_union_eq Constr.equal binders_to_remove_from_t binders_to_remove_from_v) @@ -250,8 +251,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in it_mkProd_or_LetIn (it_mkProd_or_LetIn - pre_res (List.map (function Context.Named.Declaration.LocalAssum (id,b) -> LocalAssum (Name (Hashtbl.find tbl id), b) - | Context.Named.Declaration.LocalDef (id,t,b) -> LocalDef (Name (Hashtbl.find tbl id), t, b)) + pre_res (List.map (function + | Context.Named.Declaration.LocalAssum (id,b) -> + LocalAssum (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, b) + | Context.Named.Declaration.LocalDef (id,t,b) -> + LocalDef (map_annot (fun id -> Name.mk_name (Hashtbl.find tbl id)) id, t, b)) new_predicates) ) (List.map (fun d -> Termops.map_rel_decl EConstr.Unsafe.to_constr d) princ_type_info.params) @@ -264,7 +268,7 @@ let change_property_sort evd toSort princ princName = let princ_info = compute_elim_sig evd princ in let change_sort_in_predicate decl = LocalAssum - (get_name decl, + (get_annot decl, let args,ty = decompose_prod (EConstr.Unsafe.to_constr (get_type decl)) in let s = destSort ty in Global.add_constraints (Univ.enforce_leq (univ_of_sort toSort) (univ_of_sort s) Univ.Constraint.empty); @@ -304,26 +308,30 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin 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 + let pstate = + Lemmas.start_proof ~ontop:None 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 - ; - (* let _tim1 = System.get_time () in *) - let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in - ignore (Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams))); - (* 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; *) - get_proof_clean true, CEphemeron.create hook - end - + in + (* let _tim1 = System.get_time () in *) + let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in + let pstate,_ = Pfedit.by (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)) pstate 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 open Proof_global in + let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in + match entries with + | [entry] -> + let pstate = discard_current pstate in + (id,(entry,persistence)), hook, pstate + | _ -> + CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term") let generate_functional_principle (evd: Evd.evar_map ref) interactive_proof @@ -348,7 +356,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) in let names = ref [new_princ_name] in let hook = - fun new_principle_type _ _ -> + fun new_principle_type _ _ _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) @@ -359,10 +367,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) 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.univ_entry ~poly:false evd' in let ce = Declare.definition_entry ~univs value in ignore( Declare.declare_constant @@ -376,32 +381,17 @@ let generate_functional_principle (evd: Evd.evar_map ref) register_with_sort InProp; register_with_sort InSet in - let ((id,(entry,g_kind)),hook) = + let ((id,(entry,g_kind)),hook,pstate) = build_functional_principle evd interactive_proof old_princ_type new_sorts funs i proof_tac hook in (* Pr 1278 : Don't forget to close the goal if an error is raised !!!! *) - save false new_princ_name entry g_kind hook + let uctx = Evd.evar_universe_context sigma in + save new_princ_name entry ~hook uctx g_kind with e when CErrors.noncritical e -> - begin - begin - try - let id = Proof_global.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Proof_global.discard_current () - else () - else () - with e when CErrors.noncritical e -> () - end; - raise (Defining_principle e) - end -(* defined () *) - + raise (Defining_principle e) exception Not_Rec @@ -411,7 +401,7 @@ let get_funs_constant mp = | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> - match na with + match na.binder_name with | Name id -> let const = Constant.make2 mp (Label.of_id id) in const,i @@ -448,7 +438,8 @@ let get_funs_constant mp = let first_params = List.hd l_params in List.iter (fun params -> - if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && Constr.equal c1 c2) first_params params) + if not (List.equal (fun (n1, c1) (n2, c2) -> + eq_annot Name.equal n1 n2 && Constr.equal c1 c2) first_params params) then user_err Pp.(str "Not a mutal recursive block") ) l_params @@ -458,7 +449,7 @@ let get_funs_constant mp = try let extract_info is_first body = match Constr.kind body with - | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) + | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca) | _ -> if is_first && Int.equal (List.length l_bodies) 1 then raise Not_Rec @@ -466,9 +457,9 @@ let get_funs_constant mp = in let first_infos = extract_info true (List.hd l_bodies) in let check body = (* Hope this is correct *) - let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = - Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 && - Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 + let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) = + Array.equal Int.equal ia1 ia2 && Array.equal (eq_annot Name.equal) na1 na2 && + Array.equal Constr.equal ta1 ta2 && Array.equal Constr.equal ca1 ca2 in if not (eq_infos first_infos (extract_info false body)) then user_err Pp.(str "Not a mutal recursive block") @@ -529,7 +520,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ s::l_schemes -> s,l_schemes | _ -> anomaly (Pp.str "") in - let ((_,(const,_)),_) = + let ((_,(const,_)),_,pstate) = try build_functional_principle evd false first_type @@ -537,23 +528,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs 0 (prove_princ_for_struct evd false 0 (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) with e when CErrors.noncritical e -> - begin - begin - try - let id = Proof_global.get_current_proof_name () in - let s = Id.to_string id in - let n = String.length "___________princ_________" in - if String.length s >= n - then if String.equal (String.sub s 0 n) "___________princ_________" - then Proof_global.discard_current () - else () - else () - with e when CErrors.noncritical e -> () - end; - raise (Defining_principle e) - end + raise (Defining_principle e) in incr i; @@ -603,7 +580,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ (* If we reach this point, the two principle are not mutually recursive We fall back to the previous method *) - let ((_,(const,_)),_) = + let ((_,(const,_)),_,pstate) = build_functional_principle evd false @@ -612,7 +589,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ this_block_funs !i (prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs))) - (fun _ _ _ -> ()) + (fun _ _ _ _ _ -> ()) in const with Found_type i -> @@ -676,11 +653,15 @@ 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_qualid f) in - let first_fun,u = destConst funs 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 first_fun in @@ -688,7 +669,7 @@ let build_case_scheme fa = 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 @@ -700,7 +681,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) -> - UnivGen.new_sort_in_family x + fst @@ UnivGen.fresh_sort_in_family x ) fa in @@ -718,7 +699,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/g_indfun.ml4 b/plugins/funind/g_indfun.mlg index a2d31780dd..4e8cf80ed2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.mlg @@ -7,27 +7,32 @@ (* * 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 Tacarg open Tactypes -open Pcoq open Pcoq.Prim open Pcoq.Constr open Pltac +} + DECLARE PLUGIN "recdef_plugin" -let pr_fun_ind_using prc prlc _ opt_c = +{ + +let pr_fun_ind_using env sigma prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -42,28 +47,29 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = 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) + spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) 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 env sigma } + GLOB_PRINTED BY { pr_fun_ind_using env sigma } +| [ "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 -> @@ -75,57 +81,70 @@ 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 +let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma) + +} 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 env sigma } +| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l } +| [ constr(c) ] -> { [c] } END -let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc +{ + +let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma) + +} 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 env sigma } +| [ "using" constr_comma_sequence'(l) ] -> { l } +| [ ] -> { [] } END -module Gram = Pcoq.Gram +{ + module Vernac = Pvernac.Vernac_ module Tactic = Pltac @@ -137,45 +156,56 @@ 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 + 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 +} + (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function - ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] - => [ let hard = List.exists (function +| ![ proof ] ["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 (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_qualid fun_name ++ spc() ++ str "Sort " ++ - Termops.pr_sort_family s + 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 @@ -190,50 +220,49 @@ let warning_error names e = 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 ] +| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ] + => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) } -> - [ + { fun ~pstate -> begin - try - Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - begin - match fas with - | (_,fun_name,_)::_ -> - begin - begin - make_graph (Smartlocate.global_with_alias fun_name) - end - ; - try Functional_principles_types.build_scheme fas - with Functional_principles_types.No_graph_found -> - CErrors.user_err Pp.(str "Cannot generate induction principle(s)") - | e when CErrors.noncritical e -> - let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e - - end + try + Functional_principles_types.build_scheme fas; pstate + with + | Functional_principles_types.No_graph_found -> + begin + match fas with + | (_,fun_name,_)::_ -> + begin + let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in + try Functional_principles_types.build_scheme fas; pstate + with + | Functional_principles_types.No_graph_found -> + CErrors.user_err Pp.(str "Cannot generate induction principle(s)") + | e when CErrors.noncritical e -> + let names = List.map (fun (_,na,_) -> na) fas in + warning_error names e; pstate + end | _ -> assert false (* we can only have non empty list *) - end - | e when CErrors.noncritical e -> - let names = List.map (fun (_,na,_) -> na) fas in - warning_error names e + end + | e when CErrors.noncritical e -> + let names = List.map (fun (_,na,_) -> na) fas in + warning_error names e; pstate 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) ] +| ![ proof ] ["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 7c80b776a4..275b58f0aa 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -2,6 +2,7 @@ open Printer open Pp open Names open Constr +open Context open Vars open Glob_term open Glob_ops @@ -321,12 +322,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) @@ -345,20 +344,21 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let typ,_ = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in + let na = make_annot id Sorts.Relevant in (* TODO relevance *) (match raw_value with | None -> - EConstr.push_named (NamedDecl.LocalAssum (id,typ)) env + EConstr.push_named (NamedDecl.LocalAssum (na,typ)) env | Some value -> - EConstr.push_named (NamedDecl.LocalDef (id, value, typ)) env) + EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env) -let add_pat_variables pat typ env : Environ.env = +let add_pat_variables sigma pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match DAst.get pat with - | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env + | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (make_annot na Sorts.Relevant,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ) @@ -369,24 +369,25 @@ let add_pat_variables pat typ env : Environ.env = let cs_args_types :types list = List.map RelDecl.get_type constructor.Inductiveops.cs_args in List.fold_left2 add_pat_variables env patl (List.rev cs_args_types) in - let new_env = add_pat_variables env pat typ in + let new_env = add_pat_variables env pat typ in let res = fst ( Context.Rel.fold_outside (fun decl (env,ctxt) -> let open Context.Rel.Declaration in - let sigma, _ = Pfedit.get_current_context () in match decl with - | LocalAssum (Anonymous,_) | LocalDef (Anonymous,_,_) -> assert false - | LocalAssum (Name id, t) -> + | LocalAssum ({binder_name=Anonymous},_) | LocalDef ({binder_name=Anonymous},_,_) -> assert false + | LocalAssum ({binder_name=Name id} as na, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr_env env sigma t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (id,new_t)) env,mkVar id::ctxt) - | LocalDef (Name id, v, t) -> + (Environ.push_named (LocalAssum (na,new_t)) env,mkVar id::ctxt) + | LocalDef ({binder_name=Name id} as na, v, t) -> + let na = {na with binder_name=id} in let new_t = substl ctxt t in let new_v = substl ctxt v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ @@ -396,7 +397,7 @@ let add_pat_variables pat typ env : Environ.env = str "new value := " ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalDef (id,new_v,new_t)) env,mkVar id::ctxt) + (Environ.push_named (LocalDef (na,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -474,11 +475,11 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function *) -let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = +let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr_env env rt); let open CAst in match DAst.get rt with - | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid | GApp(_,_) -> @@ -486,7 +487,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let args_res : (glob_constr list) build_entry_return = List.fold_right (* create the arguments lists of constructors and combine them *) (fun arg ctxt_argsl -> - let arg_res = build_entry_lc env funnames ctxt_argsl.to_avoid arg in + let arg_res = build_entry_lc env sigma funnames ctxt_argsl.to_avoid arg in combine_results combine_args arg_res ctxt_argsl ) args @@ -505,7 +506,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | _ -> GApp(t,l) in - build_entry_lc env funnames avoid (aux f args) + build_entry_lc env sigma funnames avoid (aux f args) | GVar id when Id.Set.mem id funnames -> (* if we have [f t1 ... tn] with [f]$\in$[fnames] then we create a fresh variable [res], @@ -569,7 +570,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = in build_entry_lc env - funnames + sigma + funnames avoid (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> @@ -577,7 +579,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = we first compute the result from the case and then combine each of them with each of args one *) - let f_res = build_entry_lc env funnames args_res.to_avoid f in + let f_res = build_entry_lc env sigma funnames args_res.to_avoid f in combine_results combine_app f_res args_res | GCast(b,_) -> (* for an applied cast we just trash the cast part @@ -585,9 +587,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = WARNING: We need to restart since [b] itself should be an application term *) - build_entry_lc env funnames avoid (mkGApp(b,args)) + build_entry_lc env sigma funnames avoid (mkGApp(b,args)) | GRec _ -> user_err Pp.(str "Not handled GRec") | GProd _ -> user_err Pp.(str "Cannot apply a type") + | GInt _ -> user_err Pp.(str "Cannot apply an integer") end (* end of the application treatement *) | GLambda(n,_,t,b) -> @@ -596,14 +599,14 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the type and combine the two result *) - let t_res = build_entry_lc env funnames avoid t in + let t_res = build_entry_lc env sigma funnames avoid t in let new_n = match n with | Name _ -> n | Anonymous -> Name (Indfun_common.fresh_id [] "_x") in let new_env = raw_push_named (new_n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in + let b_res = build_entry_lc new_env sigma funnames avoid b in combine_results (combine_lam new_n) t_res b_res | GProd(n,_,t,b) -> (* we first compute the list of constructor @@ -611,9 +614,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the type and combine the two result *) - let t_res = build_entry_lc env funnames avoid t in + let t_res = build_entry_lc env sigma funnames avoid t in let new_env = raw_push_named (n,None,t) env in - let b_res = build_entry_lc new_env funnames avoid b in + let b_res = build_entry_lc new_env sigma funnames avoid b in if List.length t_res.result = 1 && List.length b_res.result = 1 then combine_results (combine_prod2 n) t_res b_res else combine_results (combine_prod n) t_res b_res @@ -624,22 +627,23 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in - let v_res = build_entry_lc env funnames avoid v in + let v_res = build_entry_lc env sigma funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in + let v_r = Sorts.Relevant in (* TODO relevance *) let new_env = match n with Anonymous -> env - | Name id -> EConstr.push_named (NamedDecl.LocalDef (id,v_as_constr,v_type)) env - in - let b_res = build_entry_lc new_env funnames avoid b in + | Name id -> EConstr.push_named (NamedDecl.LocalDef (make_annot id v_r,v_as_constr,v_type)) env + in + let b_res = build_entry_lc new_env sigma funnames avoid b in combine_results (combine_letin n) v_res b_res | GCases(_,_,el,brl) -> (* we create the discrimination function and treat the case itself *) let make_discr = make_discr_match brl in - build_entry_lc_from_case env funnames make_discr el brl avoid + build_entry_lc_from_case env sigma funnames make_discr el brl avoid | GIf(b,(na,e_option),lhs,rhs) -> let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in @@ -662,7 +666,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = mkGCases(None,[(b,(Anonymous,None))],brl) in (* Pp.msgnl (str "new case := " ++ Printer.pr_glob_constr match_expr); *) - build_entry_lc env funnames avoid match_expr + build_entry_lc env sigma funnames avoid match_expr | GLetTuple(nal,_,b,e) -> begin let nal_as_glob_constr = @@ -686,13 +690,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = assert (Int.equal (Array.length case_pats) 1); let br = CAst.make ([],[case_pats.(0)],e) in let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in - build_entry_lc env funnames avoid match_expr + build_entry_lc env sigma funnames avoid match_expr end | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,_) -> - build_entry_lc env funnames avoid b -and build_entry_lc_from_case env funname make_discr + build_entry_lc env sigma funnames avoid b +and build_entry_lc_from_case env sigma funname make_discr (el:tomatch_tuples) (brl:Glob_term.cases_clauses) avoid : glob_constr build_entry_return = @@ -710,7 +714,7 @@ and build_entry_lc_from_case env funname make_discr let case_resl = List.fold_right (fun (case_arg,_) ctxt_argsl -> - let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in + let arg_res = build_entry_lc env sigma funname ctxt_argsl.to_avoid case_arg in combine_results combine_args arg_res ctxt_argsl ) el @@ -727,7 +731,7 @@ and build_entry_lc_from_case env funname make_discr List.map (fun ca -> let res = build_entry_lc_from_case_term - env types + env sigma types funname (make_discr) [] brl case_resl.to_avoid @@ -744,7 +748,7 @@ and build_entry_lc_from_case env funname make_discr [] results } -and build_entry_lc_from_case_term env types funname make_discr patterns_to_prevent brl avoid +and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to_prevent brl avoid matched_expr = match brl with | [] -> (* computed_branches *) {result = [];to_avoid = avoid} @@ -755,14 +759,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (* building a list of precondition stating that we are not in this branch (will be used in the following recursive calls) *) - let new_env = List.fold_right2 add_pat_variables patl types env in + let new_env = List.fold_right2 (add_pat_variables sigma) patl types env in let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list = List.map2 (fun pat typ -> fun avoid pat'_as_term -> let renamed_pat,_,_ = alpha_pat avoid pat in let pat_ids = get_pattern_id renamed_pat in - let env_with_pat_ids = add_pat_variables pat typ new_env in + let env_with_pat_ids = add_pat_variables sigma pat typ new_env in List.fold_right (fun id acc -> let typ_of_id = @@ -794,6 +798,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let brl'_res = build_entry_lc_from_case_term env + sigma types funname make_discr @@ -858,7 +863,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve ) in (* We compute the result of the value returned by the branch*) - let return_res = build_entry_lc new_env funname new_avoid return in + let return_res = build_entry_lc new_env sigma funname new_avoid return in (* and combine it with the preconds computed for this branch *) let this_branch_res = List.map @@ -891,8 +896,7 @@ let same_raw_term rt1 rt2 = | GRef(r1,_), GRef (r2,_) -> GlobRef.equal r1 r2 | GHole _, GHole _ -> true | _ -> false -let decompose_raw_eq lhs rhs = - let _, env = Pfedit.get_current_context () in +let decompose_raw_eq env lhs rhs = let rec decompose_raw_eq lhs rhs acc = observe (str "decomposing eq for " ++ pr_glob_constr_env env lhs ++ str " " ++ pr_glob_constr_env env rhs); let (rhd,lrhs) = glob_decompose_app rhs in @@ -940,9 +944,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in - let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -975,9 +980,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_args = List.map (replace_var_by_term id rt) args in let subst_b = if is_in_b then b else replace_var_by_term id rt b - in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + in + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1058,8 +1064,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = in let new_env = let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in - EConstr.push_rel (LocalAssum (n,t')) env - in + let r = Sorts.Relevant in (* TODO relevance *) + EConstr.push_rel (LocalAssum (make_annot n r,t')) env + in let new_b,id_to_exclude = rebuild_cons new_env @@ -1079,7 +1086,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = -> begin try - let l = decompose_raw_eq rt1 rt2 in + let l = decompose_raw_eq env rt1 rt2 in if List.length l > 1 then let new_rt = @@ -1096,8 +1103,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1112,8 +1120,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr_env env rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args new_crossed_types @@ -1133,8 +1142,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> - let new_env = EConstr.push_rel (LocalAssum (n,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot n r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname (args@[mkGVar id])new_crossed_types @@ -1159,7 +1169,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let type_t' = Typing.unsafe_type_of env evd t' in let t' = EConstr.Unsafe.to_constr t' in let type_t' = EConstr.Unsafe.to_constr type_t' in - let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in + let new_env = Environ.push_rel (LocalDef (make_annot n Sorts.Relevant,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1183,8 +1193,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = depth t in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = EConstr.push_rel (LocalAssum (na,t')) env in - let new_b,id_to_exclude = + let r = Sorts.Relevant in (* TODO relevance *) + let new_env = EConstr.push_rel (LocalAssum (make_annot na r,t')) env in + let new_b,id_to_exclude = rebuild_cons new_env nb_args relname args (t::crossed_types) @@ -1221,7 +1232,7 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) let rec compute_cst_params relnames params gt = DAst.with_val (function - | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params + | GRef _ | GVar _ | GEvar _ | GPatVar _ | GInt _ -> params | GApp(f,args) -> begin match DAst.get f with | GVar relname' when Id.Set.mem relname' relnames -> @@ -1321,7 +1332,7 @@ let do_build_inductive let evd,t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in let t = EConstr.Unsafe.to_constr t in evd, - Environ.push_named (LocalAssum (id,t)) + Environ.push_named (LocalAssum (make_annot id Sorts.Relevant,t)) env ) funnames @@ -1335,7 +1346,7 @@ let do_build_inductive resolve_and_replace_implicits ~expected_type:(Pretyping.OfType t) env evd rt ) rta in - let resa = Array.map (build_entry_lc env funnames_as_set []) rta in + let resa = Array.map (build_entry_lc env evd funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = @@ -1365,7 +1376,8 @@ let do_build_inductive Util.Array.fold_left2 (fun env rel_name rel_ar -> let rex = fst (with_full_print (Constrintern.interp_constr env evd) rel_ar) in let rex = EConstr.Unsafe.to_constr rex in - Environ.push_named (LocalAssum (rel_name,rex)) env) env relnames rel_arities + let r = Sorts.Relevant in (* TODO relevance *) + Environ.push_named (LocalAssum (make_annot rel_name r,rex)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1494,7 +1506,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (ComInductive.do_mutual_inductive ~template:None None rel_inds (Flags.is_universe_polymorphism ()) false false ~uniform:ComInductive.NonUniformParameters)) + (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters)) Declarations.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5b45a8dbed..13ff19a46b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -106,6 +106,7 @@ let change_vars = | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported") | GSort _ as x -> x | GHole _ as x -> x + | GInt _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, Glob_ops.map_cast_type (change_vars mapping) c) @@ -285,6 +286,7 @@ let rec alpha_rt excluded rt = ) | GRec _ -> user_err Pp.(str "Not handled GRec") | GSort _ + | GInt _ | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, @@ -344,6 +346,7 @@ 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 + | GInt _ -> false ) x and is_free_in_br {CAst.v=(ids,_,rt)} = (not (Id.List.mem id ids)) && is_free_in rt @@ -434,6 +437,7 @@ let replace_var_by_term x_id term = | GRec _ -> raise (UserError(None,str "Not handled GRec")) | GSort _ | GHole _ as rt -> rt + | GInt _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, Glob_ops.map_cast_type replace_var_by_pattern c) @@ -516,7 +520,7 @@ let expand_as = | PatCstr(_,patl,_) -> List.fold_left add_as map patl in let rec expand_as map = DAst.map (function - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ as rt -> rt | GVar id as rt -> begin try diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9a6169d42a..a5c19f3217 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -3,6 +3,7 @@ open Sorts open Util open Names open Constr +open Context open EConstr open Pp open Indfun_common @@ -49,7 +50,8 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction information on "++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') ) in - match Tacticals.elimination_sort_of_goal g with + match Tacticals.elimination_sort_of_goal g with + | InSProp -> finfo.sprop_lemma | InProp -> finfo.prop_lemma | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma @@ -166,10 +168,11 @@ let build_newrecursive let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in - let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars ~program_mode:false env evd bl in let impl = Constrintern.compute_internalization_data env0 evd Constrintern.Recursive arity impls' in let open Context.Named.Declaration in - (EConstr.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) + let r = Sorts.Relevant in (* TODO relevance *) + (EConstr.push_named (LocalAssum (make_annot recname r,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) @@ -201,7 +204,7 @@ let is_rec names = let check_id id names = Id.Set.mem id names in let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names - | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false + | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ | GInt _ -> false | GCast(b,_) -> lookup names b | GRec _ -> error "GRec not handled" | GIf(b,_,lhs,rhs) -> @@ -407,15 +410,15 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error with e when CErrors.noncritical e -> on_error names e -let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = +let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - ComDefinition.do_definition + ComDefinition.do_definition ~ontop:pstate ~program_mode:false fname - (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl - bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); + (Decl_kinds.Global,false,Decl_kinds.Definition) pl + bl None body (Some ret_type); let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -429,9 +432,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - evd,List.rev rev_pconstants + pstate, evd,List.rev rev_pconstants | _ -> - ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in let evd,rev_pconstants = List.fold_left (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> @@ -445,8 +448,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Evd.from_env (Global.env ()),[]) fixpoint_exprl in - evd,List.rev rev_pconstants - + pstate,evd,List.rev rev_pconstants + let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation @@ -621,8 +624,8 @@ let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in - let constr_expr_typel = + let ((_,_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in + let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> @@ -635,10 +638,10 @@ 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 - (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit = +let do_generate_principle ~pstate pconstants on_error register_built interactive_proof + (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option = List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl; - let _is_struct = + let pstate, _is_struct = match fixpoint_exprl with | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = @@ -662,8 +665,8 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; - false + then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, false + else pstate, false |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with @@ -686,8 +689,8 @@ 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 name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true + else pstate, true | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> match ord with @@ -704,10 +707,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in - let evd,pconstants = + let pstate,evd,pconstants = if register_built - then register_struct is_rec fixpoint_exprl - else (Evd.from_env (Global.env ()),pconstants) + then register_struct ~pstate is_rec fixpoint_exprl + else pstate, Evd.from_env (Global.env ()), pconstants in let evd = ref evd in generate_principle @@ -720,10 +723,11 @@ let do_generate_principle pconstants on_error register_built interactive_proof recdefs interactive_proof (Functional_principles_proofs.prove_princ_for_struct evd interactive_proof); - if register_built then begin derive_inversion fix_names; end; - true; + if register_built then + begin derive_inversion fix_names; end; + pstate, true in - () + pstate let rec add_args id new_args = CAst.map (function | CRef (qid,_) as b -> @@ -840,13 +844,14 @@ let rec get_args b t : Constrexpr.local_binder_expr list * | _ -> [],b,t -let make_graph (f_ref : GlobRef.t) = +let make_graph ~pstate (f_ref : GlobRef.t) = + let sigma, env = Option.cata Pfedit.get_current_context + (let e = Global.env () in Evd.from_env e, e) pstate in let c,c_body = match f_ref with | ConstRef c -> begin try c,Global.lookup_constant c with Not_found -> - let sigma, env = Pfedit.get_current_context () in raise (UserError (None,str "Cannot find " ++ Printer.pr_leconstr_env env sigma (mkConst c)) ) end | _ -> raise (UserError (None, str "Not a function reference") ) @@ -854,8 +859,7 @@ let make_graph (f_ref : GlobRef.t) = (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom!" | Some (body, _) -> - let env = Global.env () in - let sigma = Evd.from_env env in + let env = Global.env () in let extern_body,extern_type = with_full_print (fun () -> (Constrextern.extern_constr false env sigma (EConstr.of_constr body), @@ -899,12 +903,11 @@ let make_graph (f_ref : GlobRef.t) = [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp = Constant.modpath c in - do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; + let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in (* We register the infos *) List.iter (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id))) - expr_list) + expr_list; + pstate) let do_generate_principle = do_generate_principle [] warning_error true - - diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index f209fb19fd..acf85f539e 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -5,18 +5,16 @@ 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 : pstate:Proof_global.t option -> + bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + Proof_global.t option -val functional_induction : +val functional_induction : bool -> EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Ltac_plugin.Tacexpr.or_and_intro_pattern option -> Goal.goal Evd.sigma -> Goal.goal list Evd.sigma - -val make_graph : GlobRef.t -> unit +val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 03a64988e4..40f66ce5eb 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -27,10 +27,6 @@ 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 qid = Nametab.locate qid let locate_ind ref = @@ -105,18 +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 - 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 = - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s;; @@ -142,7 +129,7 @@ let get_locality = function | Local -> true | Global -> false -let save with_clean id const (locality,_,kind) hook = +let save id const ?hook uctx (locality,_,kind) = let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> @@ -156,21 +143,9 @@ let save with_clean id const (locality,_,kind) hook = let kn = declare_constant id ~local (DefinitionEntry const, k) in (locality, ConstRef kn) in - if with_clean then Proof_global.discard_current (); - CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + Lemmas.call_hook ?hook ~fix_exn uctx [] 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 () @@ -223,6 +198,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -261,7 +237,6 @@ let cache_Function (_,finfos) = from_graph := Indmap.add finfos.graph_ind finfos !from_graph -let load_Function _ = cache_Function let subst_Function (subst,finfos) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst_ind i = Mod_subst.subst_ind subst i @@ -274,6 +249,7 @@ let subst_Function (subst,finfos) = 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 + let sprop_lemma' = Option.Smart.map do_subst_con finfos.sprop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -281,7 +257,8 @@ let subst_Function (subst,finfos) = completeness_lemma' == finfos.completeness_lemma && rect_lemma' == finfos.rect_lemma && rec_lemma' == finfos.rec_lemma && - prop_lemma' == finfos.prop_lemma + prop_lemma' == finfos.prop_lemma && + sprop_lemma' == finfos.sprop_lemma then finfos else { function_constant = function_constant'; @@ -292,49 +269,41 @@ let subst_Function (subst,finfos) = rect_lemma = rect_lemma' ; rec_lemma = rec_lemma'; prop_lemma = prop_lemma'; + sprop_lemma = sprop_lemma'; is_general = finfos.is_general } -let classify_Function infos = Libobject.Substitute infos - - let discharge_Function (_,finfos) = Some finfos -let pr_ocst c = - let sigma, env = Pfedit.get_current_context () in +let pr_ocst env sigma c = Option.fold_right (fun v acc -> Printer.pr_lconstr_env env sigma (mkConst v)) c (mt ()) -let pr_info f_info = - let sigma, env = Pfedit.get_current_context () in +let pr_info env sigma f_info = str "function_constant := " ++ Printer.pr_lconstr_env env sigma (mkConst f_info.function_constant)++ fnl () ++ 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 () ++ - str "correctness_lemma := " ++ pr_ocst f_info.correctness_lemma ++ fnl () ++ - str "rect_lemma := " ++ pr_ocst f_info.rect_lemma ++ fnl () ++ - str "rec_lemma := " ++ pr_ocst f_info.rec_lemma ++ fnl () ++ - str "prop_lemma := " ++ pr_ocst f_info.prop_lemma ++ fnl () ++ + str "equation_lemma := " ++ pr_ocst env sigma f_info.equation_lemma ++ fnl () ++ + str "completeness_lemma :=" ++ pr_ocst env sigma f_info.completeness_lemma ++ fnl () ++ + str "correctness_lemma := " ++ pr_ocst env sigma f_info.correctness_lemma ++ fnl () ++ + str "rect_lemma := " ++ pr_ocst env sigma f_info.rect_lemma ++ fnl () ++ + str "rec_lemma := " ++ pr_ocst env sigma f_info.rec_lemma ++ fnl () ++ + str "prop_lemma := " ++ pr_ocst env sigma f_info.prop_lemma ++ fnl () ++ str "graph_ind := " ++ Printer.pr_lconstr_env env sigma (mkInd f_info.graph_ind) ++ fnl () -let pr_table tb = +let pr_table env sigma tb = let l = Cmap_env.fold (fun k v acc -> v::acc) tb [] in - Pp.prlist_with_sep fnl pr_info l + Pp.prlist_with_sep fnl (pr_info env sigma) l let in_Function : function_info -> Libobject.obj = - Libobject.declare_object - {(Libobject.default_object "FUNCTIONS_DB") with - Libobject.cache_function = cache_Function; - Libobject.load_function = load_Function; - Libobject.classify_function = classify_Function; - Libobject.subst_function = subst_Function; - Libobject.discharge_function = discharge_Function -(* Libobject.open_function = open_Function; *) - } + let open Libobject in + declare_object @@ superglobal_object "FUNCTIONS_DB" + ~cache:cache_Function + ~subst:(Some subst_Function) + ~discharge:discharge_Function let find_or_none id = @@ -365,6 +334,7 @@ let add_Function is_general f = and rect_lemma = find_or_none (Nameops.add_suffix f_id "_rect") and rec_lemma = find_or_none (Nameops.add_suffix f_id "_rec") and prop_lemma = find_or_none (Nameops.add_suffix f_id "_ind") + and sprop_lemma = find_or_none (Nameops.add_suffix f_id "_sind") and graph_ind = match Nametab.locate (qualid_of_ident (mk_rel_id f_id)) with | IndRef ind -> ind | _ -> CErrors.anomaly (Pp.str "Not an inductive.") @@ -377,6 +347,7 @@ let add_Function is_general f = rect_lemma = rect_lemma; rec_lemma = rec_lemma; prop_lemma = prop_lemma; + sprop_lemma = sprop_lemma; graph_ind = graph_ind; is_general = is_general @@ -384,7 +355,7 @@ let add_Function is_general f = in update_Function finfos -let pr_table () = pr_table !from_function +let pr_table env sigma = pr_table env sigma !from_function (*********************************) (* Debuging *) let functional_induction_rewrite_dependent_proofs = ref true @@ -399,7 +370,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 @@ -412,7 +383,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 @@ -430,7 +401,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 @@ -441,7 +412,7 @@ let jmeq () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.type" with e when CErrors.noncritical e -> raise (ToShow e) @@ -449,7 +420,7 @@ let jmeq_refl () = try Coqlib.check_required_library Coqlib.jmeq_module_name; EConstr.of_constr @@ - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.JMeq.refl" with e when CErrors.noncritical e -> raise (ToShow e) @@ -463,7 +434,7 @@ let acc_rel = function () -> EConstr.of_constr (coq_constant "Acc") let acc_inv_id = function () -> EConstr.of_constr (coq_constant "Acc_inv") [@@@ocaml.warning "-3"] -let well_founded_ltof () = EConstr.of_constr @@ UnivGen.constr_of_global @@ +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"] @@ -524,7 +495,7 @@ type tcc_lemma_value = (* We only "purify" on exceptions. XXX: What is this doing here? *) let funind_purify f x = - let st = Vernacstate.freeze_interp_state `No in + let st = Vernacstate.freeze_interp_state ~marshallable:false in try f x with e -> let e = CErrors.push e in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7e52ee224f..9670cf1fa7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -18,8 +18,6 @@ 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.qualid -> inductive val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : @@ -38,24 +36,19 @@ 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 -> 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) - - +val save + : Id.t + -> Safe_typing.private_constants Entries.definition_entry + -> ?hook:Lemmas.declaration_hook + -> UState.t + -> Decl_kinds.goal_kind + -> unit (* [with_full_print f a] applies [f] to [a] in full printing environment. @@ -76,6 +69,7 @@ type function_info = rect_lemma : Constant.t option; rec_lemma : Constant.t option; prop_lemma : Constant.t option; + sprop_lemma : Constant.t option; is_general : bool; } @@ -83,14 +77,11 @@ val find_Function_infos : Constant.t -> function_info val find_Function_of_graph : inductive -> function_info (* WARNING: To be used just after the graph definition !!! *) val add_Function : bool -> Constant.t -> unit - val update_Function : function_info -> unit - (** debugging *) -val pr_info : function_info -> Pp.t -val pr_table : unit -> Pp.t - +val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t +val pr_table : Environ.env -> Evd.evar_map -> Pp.t (* val function_debug : bool ref *) val do_observe : unit -> bool @@ -115,9 +106,9 @@ val evaluable_of_global_reference : GlobRef.t -> Names.evaluable_global_referenc val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic val decompose_lam_n : Evd.evar_map -> int -> EConstr.t -> - (Names.Name.t * EConstr.t) list * EConstr.t -val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t -val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t + (Names.Name.t Context.binder_annot * EConstr.t) list * EConstr.t +val compose_lam : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t +val compose_prod : (Names.Name.t Context.binder_annot * EConstr.t) list -> EConstr.t -> EConstr.t type tcc_lemma_value = | Undefined diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b8973a18dc..edb698280f 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -15,6 +15,7 @@ open Util open Names open Term open Constr +open Context open EConstr open Vars open Pp @@ -63,12 +64,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.from_env Environ.empty_env) - 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,7 +76,7 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl let make_eq () = try - EConstr.of_constr (UnivGen.constr_of_global (Coqlib.lib_ref "core.eq.type")) + 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] @@ -148,12 +143,13 @@ let generate_type evd g_to_f f graph i = \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res, \] i*) let pre_ctxt = - LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt + LocalAssum (make_annot (Name res_id) Sorts.Relevant, lift 1 res_type) :: + LocalDef (make_annot (Name fv_id) Sorts.Relevant, mkApp (f,args_as_rels), res_type) :: fun_ctxt in (*i and we can return the solution depending on which lemma type we are defining i*) if g_to_f - then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph - else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph + then LocalAssum (make_annot Anonymous Sorts.Relevant,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph + else LocalAssum (make_annot Anonymous Sorts.Relevant,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph (* @@ -219,7 +215,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 @@ -276,10 +272,10 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let type_of_hid = pf_unsafe_type_of g (mkVar hid) in let sigma = project g in match EConstr.kind sigma type_of_hid with - | Prod(_,_,t') -> + | Prod(_,_,t') -> begin match EConstr.kind sigma t' with - | Prod(_,t'',t''') -> + | Prod(_,t'',t''') -> begin match EConstr.kind sigma t'',EConstr.kind sigma t''' with | App(eq,args), App(graph',_) @@ -364,17 +360,16 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i (* end of branche proof *) let lemmas = Array.map - (fun ((_,(ctxt,concl))) -> - match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") - | hres::res::decl::ctxt -> - let res = EConstr.it_mkLambda_or_LetIn - (EConstr.it_mkProd_or_LetIn concl [hres;res]) - (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt) - in - res - ) - lemmas_types_infos + (fun ((_,(ctxt,concl))) -> + match ctxt with + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") + | hres::res::decl::ctxt -> + let res = EConstr.it_mkLambda_or_LetIn + (EConstr.it_mkProd_or_LetIn concl [hres;res]) + (LocalAssum (RelDecl.get_annot decl, RelDecl.get_type decl) :: ctxt) + in + res) + lemmas_types_infos in let param_names = fst (List.chop princ_infos.nparams args_names) in let params = List.map mkVar param_names in @@ -397,7 +392,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))) @@ -435,7 +430,7 @@ let generalize_dependent_of x hyp g = let open Context.Named.Declaration in tclMAP (function - | LocalAssum (id,t) when not (Id.equal id hyp) && + | LocalAssum ({binder_name=id},t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id]) | _ -> tclIDTAC ) @@ -462,7 +457,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = let eq_ind = make_eq () in let sigma = project g in match EConstr.kind sigma (pf_concl g) with - | Prod(_,t,t') -> + | Prod(_,t,t') -> begin match EConstr.kind sigma t with | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind) -> @@ -511,7 +506,7 @@ and intros_with_rewrite_aux : Tacmach.tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.lib_ref "core.False.type")) -> + | 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[ @@ -630,12 +625,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,7 +766,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 sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in evd := sigma; - let type_of_lemma = nf_zeta type_of_lemma in + 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 ) @@ -807,17 +802,16 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious i*) let lem_id = mk_correct_id f_id in - let (typ,_) = lemmas_types_infos.(i) in - Lemmas.start_proof + let (typ,_) = lemmas_types_infos.(i) in + let pstate = Lemmas.start_proof ~ontop:None 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 + typ in + let pstate = fst @@ Pfedit.by (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")") - (proving_tac i)))); - (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); + (proving_tac i))) pstate in + let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in 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 @@ -838,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 ) @@ -871,14 +865,13 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list Ensures by: obvious 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 - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); - ignore (Pfedit.by + let pstate = Lemmas.start_proof ~ontop:None lem_id + (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma + (fst lemmas_types_infos.(i)) in + let pstate = fst (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") - (proving_tac i)))) ; - (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)))); + (proving_tac i))) pstate) in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in 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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 89dfb58017..3c2b03dfe0 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -12,6 +12,7 @@ module CVars = Vars open Constr +open Context open EConstr open Vars open Namegen @@ -24,6 +25,7 @@ open Globnames open Nameops open CErrors open Util +open UnivGen open Tacticals open Tacmach open Tactics @@ -50,19 +52,15 @@ open Context.Rel.Declaration (* Ugly things which should not be here *) [@@@ocaml.warning "-3"] -let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@ +let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "RecursiveDefinition" m s 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 - Printer.pr_leconstr_env env sigma - let coq_init_constant s = EConstr.of_constr ( - UnivGen.constr_of_global @@ + UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) [@@@ocaml.warning "+3"] @@ -74,7 +72,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 (Proof_global.Transparent,None))) +let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None let def_of_const t = match (Constr.kind t) with @@ -96,30 +94,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.from_env env) - - -let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env - (Evd.from_env Environ.empty_env) - - - - - - (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in @@ -199,7 +179,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) = ) in let context = List.map - (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al)) + (fun (x, c) -> LocalAssum (make_annot (Name x) Sorts.Relevant, c)) (List.combine rev_x_id_l (List.rev al)) in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = @@ -248,6 +228,7 @@ let observe strm = let do_observe_tac s tac g = let goal = Printer.pr_goal g in + let s = s (pf_env g) (project g) in let lmsg = (str "recdef : ") ++ s in observe (s++fnl()); Stack.push (lmsg,goal) debug_queue; @@ -272,8 +253,8 @@ let observe_tclTHENLIST s tacl = then let rec aux n = function | [] -> tclIDTAC - | [tac] -> observe_tac (s ++ spc () ++ int n) tac - | tac::tacl -> observe_tac (s ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl)) + | [tac] -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) tac + | tac::tacl -> observe_tac (fun env sigma -> s env sigma ++ spc () ++ int n) (tclTHEN tac (aux (succ n) tacl)) in aux 0 tacl else tclTHENLIST tacl @@ -288,11 +269,11 @@ let tclUSER tac is_mes l g = | None -> tclIDTAC | Some l -> tclMAP (fun id -> tclTRY (Proofview.V82.of_tactic (clear [id]))) (List.rev l) in - observe_tclTHENLIST (str "tclUSER1") + observe_tclTHENLIST (fun _ _ -> str "tclUSER1") [ clear_tac; if is_mes - then observe_tclTHENLIST (str "tclUSER2") + then observe_tclTHENLIST (fun _ _ -> str "tclUSER2") [ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force Indfun_common.ltof_ref))]); @@ -319,10 +300,11 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = (* [check_not_nested forbidden e] checks that [e] does not contains any variable of [forbidden] *) -let check_not_nested sigma forbidden e = +let check_not_nested env sigma forbidden e = let rec check_not_nested e = match EConstr.kind sigma e with | Rel _ -> () + | Int _ -> () | Var x -> if Id.List.mem x forbidden then user_err ~hdr:"Recdef.check_not_nested" @@ -345,7 +327,6 @@ let check_not_nested sigma forbidden e = try check_not_nested e with UserError(_,p) -> - let _, env = Pfedit.get_current_context () in user_err ~hdr:"_" (str "on expr : " ++ Printer.pr_leconstr_env env sigma e ++ str " " ++ p) (* ['a info] contains the local information for traveling *) @@ -404,9 +385,9 @@ let add_vars sigma forbidden e = let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = fun g -> let rev_context,b = decompose_lam_n (project g) nb_lam e in - let ids = List.fold_left (fun acc (na,_) -> + let ids = List.fold_left (fun acc (na,_) -> let pre_id = - match na with + match na.binder_name with | Name x -> x | Anonymous -> ano_id in @@ -414,12 +395,12 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ) [] rev_context in let rev_ids = pf_get_new_ids (List.rev ids) g in let new_b = substl (List.map mkVar rev_ids) b in - observe_tclTHENLIST (str "treat_case1") + observe_tclTHENLIST (fun _ _ -> str "treat_case1") [ h_intros (List.rev rev_ids); Proofview.V82.of_tactic (intro_using teq_id); onLastHypId (fun heq -> - observe_tclTHENLIST (str "treat_case2")[ + observe_tclTHENLIST (fun _ _ -> str "treat_case2")[ Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> @@ -446,13 +427,14 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = let sigma = project g in + let env = pf_env g in match EConstr.kind sigma expr_info.info with | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint") | Proj _ -> user_err Pp.(str "Function cannot treat projections") - | LetIn(na,b,t,e) -> + | LetIn(na,b,t,e) -> begin let new_continuation_tac = - jinfo.letiN (na,b,t,e) expr_info continuation_tac + jinfo.letiN (na.binder_name,b,t,e) expr_info continuation_tac in travel jinfo new_continuation_tac {expr_info with info = b; is_final=false} g @@ -461,18 +443,18 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = | Prod _ -> begin try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end - | Lambda(n,t,b) -> + | Lambda(n,t,b) -> begin try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -500,11 +482,11 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos g - | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") - | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env (pf_env g) sigma expr_info.info ++ Pp.str ".") + | Case _ -> user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr_env env sigma expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_leconstr_env env sigma expr_info.info ++ Pp.str ".") end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g - | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> + | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ | Int _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in new_continuation_tac expr_info g @@ -522,9 +504,9 @@ and travel_args jinfo is_final continuation_tac infos = in travel jinfo new_continuation_tac {infos with info=arg;is_final=false} -and travel jinfo continuation_tac expr_info = - observe_tac - (str jinfo.message ++ pr_leconstr_rd expr_info.info) +and travel jinfo continuation_tac expr_info = + observe_tac + (fun env sigma -> str jinfo.message ++ Printer.pr_leconstr_env env sigma expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) @@ -546,16 +528,16 @@ let rec prove_lt hyple g = in let y = List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in - observe_tclTHENLIST (str "prove_lt1")[ + observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); - observe_tac (str "prove_lt") (prove_lt hyple) + observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) ] with Not_found -> ( ( - observe_tclTHENLIST (str "prove_lt2")[ + observe_tclTHENLIST (fun _ _ -> str "prove_lt2")[ Proofview.V82.of_tactic (apply (delayed_force lt_S_n)); - (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) + (observe_tac (fun _ _ -> str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption)) ]) ) end @@ -571,26 +553,26 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = let h' = next_ident_away_in_goal (h'_id) ids in let ids = h'::ids in let def = next_ident_away_in_goal def_id ids in - observe_tclTHENLIST (str "destruct_bounds_aux1")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux1")[ Proofview.V82.of_tactic (split (ImplicitBindings [s_max])); Proofview.V82.of_tactic (intro_then (fun id -> Proofview.V82.tactic begin - observe_tac (str "destruct_bounds_aux") + observe_tac (fun _ _ -> str "destruct_bounds_aux") (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id))) [ - observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id); + observe_tclTHENLIST (fun _ _ -> str "")[Proofview.V82.of_tactic (intro_using h_id); Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]))); Proofview.V82.of_tactic default_full_auto]; - observe_tclTHENLIST (str "destruct_bounds_aux2")[ - observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id])); + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux2")[ + observe_tac (fun _ _ -> str "clearing k ") (Proofview.V82.of_tactic (clear [id])); h_intros [k;h';def]; - observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); - observe_tac (str "unfold functional") + observe_tac (fun _ _ -> str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); + observe_tac (fun _ _ -> str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)])); ( - observe_tclTHENLIST (str "test")[ + observe_tclTHENLIST (fun _ _ -> str "test")[ list_rewrite true (List.fold_right (fun e acc -> (mkVar e,true)::acc) @@ -601,16 +583,16 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *) (* ; *) - (observe_tac (str "finishing") + (observe_tac (fun _ _ -> str "finishing") (tclORELSE (Proofview.V82.of_tactic intros_reflexivity) - (observe_tac (str "calling prove_lt") (prove_lt hyple))))]) + (observe_tac (fun _ _ -> str "calling prove_lt") (prove_lt hyple))))]) ] ] )end)) ] g | (_,v_bound)::l -> - observe_tclTHENLIST (str "destruct_bounds_aux3")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux3")[ Proofview.V82.of_tactic (simplest_elim (mkVar v_bound)); Proofview.V82.of_tactic (clear [v_bound]); tclDO 2 (Proofview.V82.of_tactic intro); @@ -618,7 +600,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = (fun p_hyp -> (onNthHypId 2 (fun p -> - observe_tclTHENLIST (str "destruct_bounds_aux4")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_bounds_aux4")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -642,32 +624,33 @@ let destruct_bounds infos = let terminate_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app1")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app1")[ continuation_tac infos; - observe_tac (str "first split") + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); - observe_tac (str "destruct_bounds (1)") (destruct_bounds infos) + observe_tac (fun _ _ -> str "destruct_bounds (1)") (destruct_bounds infos) ] else continuation_tac infos let terminate_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_others")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_others")[ continuation_tac infos; - observe_tac (str "first split") + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info]))); - observe_tac (str "destruct_bounds") (destruct_bounds infos) + observe_tac (fun _ _ -> str "destruct_bounds") (destruct_bounds infos) ] else continuation_tac infos let terminate_letin (na,b,t,e) expr_info continuation_tac info g = let sigma = project g in + let env = pf_env g in let new_e = subst1 info.info e in let new_forbidden = let forbid = try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) b; true with e when CErrors.noncritical e -> false in @@ -712,7 +695,7 @@ let mkDestructEq : let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: to_revert_constr in pf_typel new_hyps (fun _ -> - observe_tclTHENLIST (str "mkDestructEq") + observe_tclTHENLIST (fun _ _ -> str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> let changefun patvars env sigma = @@ -724,9 +707,10 @@ let mkDestructEq : let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in + let env = pf_env g in let f_is_present = try - check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a; + check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids) a; false with e when CErrors.noncritical e -> true @@ -740,45 +724,46 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let destruct_tac,rev_to_thin_intro = mkDestructEq [expr_info.rec_arg_id] a' g in let to_thin_intro = List.rev rev_to_thin_intro in - observe_tac (str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') + observe_tac (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') (try (tclTHENS destruct_tac - (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) + (List.map_i (fun i e -> observe_tac (fun _ _ -> str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l) )) 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 (fun _ _ -> str "is computable " ++ Printer.pr_leconstr_env env sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} ) )) g let terminate_app_rec (f,args) expr_info continuation_tac _ g = let sigma = project g in - List.iter (check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids)) + let env = pf_env g in + List.iter (check_not_nested env sigma (expr_info.f_id::expr_info.forbidden_ids)) args; begin try let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tclTHENLIST (str "terminate_app_rec")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app_rec1")[ - observe_tac (str "first split") + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec1")[ + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); - observe_tac (str "destruct_bounds (3)") + observe_tac (fun _ _ -> str "destruct_bounds (3)") (destruct_bounds new_infos) ] else tclIDTAC ] g with Not_found -> - observe_tac (str "terminate_app_rec not found") (tclTHENS + observe_tac (fun _ _ -> str "terminate_app_rec not found") (tclTHENS (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) [ - observe_tclTHENLIST (str "terminate_app_rec2")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec2")[ Proofview.V82.of_tactic (intro_using rec_res_id); Proofview.V82.of_tactic intro; onNthHypId 1 @@ -791,14 +776,14 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g = (v,v_bound)::expr_info.values_and_bounds; args_assoc=(args,mkVar v)::expr_info.args_assoc } in - observe_tclTHENLIST (str "terminate_app_rec3")[ + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec3")[ continuation_tac new_infos; if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "terminate_app_rec4")[ - observe_tac (str "first split") + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec4")[ + observe_tac (fun _ _ -> str "first split") (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info]))); - observe_tac (str "destruct_bounds (2)") + observe_tac (fun _ _ -> str "destruct_bounds (2)") (destruct_bounds new_infos) ] else @@ -808,12 +793,12 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ g = ) ) ]; - observe_tac (str "proving decreasing") ( + observe_tac (fun _ _ -> str "proving decreasing") ( tclTHENS (* proof of args < formal args *) (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv))) [ - observe_tac (str "assumption") (Proofview.V82.of_tactic assumption); - observe_tclTHENLIST (str "terminate_app_rec5") + observe_tac (fun _ _ -> str "assumption") (Proofview.V82.of_tactic assumption); + observe_tclTHENLIST (fun _ _ -> str "terminate_app_rec5") [ tclTRY(list_rewrite true (List.map @@ -849,7 +834,7 @@ let prove_terminate = travel terminate_info (* Equation proof *) let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos = - observe_tac (str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) + observe_tac (fun _ _ -> str "equation case") (terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos) let rec prove_le g = let sigma = project g in @@ -869,15 +854,15 @@ let rec prove_le g = EConstr.is_global sigma (le ()) c | _ -> false in - let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) - in + let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in + let h = h.binder_name in let y = let _,args = decompose_app sigma t in List.hd (List.tl args) in - observe_tclTHENLIST (str "prove_le")[ + observe_tclTHENLIST (fun _ _ -> str "prove_le")[ Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|]))); - observe_tac (str "prove_le (rec)") (prove_le) + observe_tac (fun _ _ -> str "prove_le (rec)") (prove_le) ] with Not_found -> tclFAIL 0 (mt()) end; @@ -887,16 +872,16 @@ let rec prove_le g = let rec make_rewrite_list expr_info max = function | [] -> tclIDTAC | (_,p,hp)::l -> - observe_tac (str "make_rewrite_list") (tclTHENS - (observe_tac (str "rewrite heq on " ++ Id.print p ) ( + observe_tac (fun _ _ -> str "make_rewrite_list") (tclTHENS + (observe_tac (fun _ _ -> str "rewrite heq on " ++ Id.print p ) ( (fun g -> let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true @@ -905,49 +890,49 @@ let rec make_rewrite_list expr_info max = function CAst.make @@ (NamedHyp k, f_S max)]) false) g) ) ) [make_rewrite_list expr_info max l; - observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *) + observe_tclTHENLIST (fun _ _ -> str "make_rewrite_list")[ (* x < S max proof *) Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm)); - observe_tac (str "prove_le(2)") prove_le + observe_tac (fun _ _ -> str "prove_le(2)") prove_le ] ] ) let make_rewrite expr_info l hp max = tclTHENFIRST - (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l)) - (observe_tac (str "make_rewrite") (tclTHENS + (observe_tac (fun _ _ -> str "make_rewrite") (make_rewrite_list expr_info max l)) + (observe_tac (fun _ _ -> str "make_rewrite") (tclTHENS (fun g -> let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in let k,def = - let k_na,_,t = destProd sigma t_eq in - let _,_,t = destProd sigma t in - let def_na,_,_ = destProd sigma t in - Nameops.Name.get_id k_na,Nameops.Name.get_id def_na + let k_na,_,t = destProd sigma t_eq in + let _,_,t = destProd sigma t in + let def_na,_,_ = destProd sigma t in + Nameops.Name.get_id k_na.binder_name,Nameops.Name.get_id def_na.binder_name in - observe_tac (str "general_rewrite_bindings") + observe_tac (fun _ _ -> str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g) - [observe_tac(str "make_rewrite finalize") ( + [observe_tac(fun _ _ -> str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) - (observe_tclTHENLIST (str "make_rewrite")[ + (observe_tclTHENLIST (fun _ _ -> str "make_rewrite")[ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); - observe_tac (str "unfold functional") + observe_tac (fun _ _ -> str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)])); (list_rewrite true (List.map (fun e -> mkVar e,true) expr_info.eqs)); - (observe_tac (str "h_reflexivity") + (observe_tac (fun _ _ -> str "h_reflexivity") (Proofview.V82.of_tactic intros_reflexivity) ) ])) ; - observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *) + observe_tclTHENLIST (fun _ _ -> str "make_rewrite1")[ (* x < S (S max) proof *) Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS))); - observe_tac (str "prove_le (3)") prove_le + observe_tac (fun _ _ -> str "prove_le (3)") prove_le ] ]) ) @@ -956,7 +941,7 @@ let rec compute_max rew_tac max l = match l with | [] -> rew_tac max | (_,p,_)::l -> - observe_tclTHENLIST (str "compute_max")[ + observe_tclTHENLIST (fun _ _ -> str "compute_max")[ Proofview.V82.of_tactic (simplest_elim (mkApp(delayed_force max_constr, [| max; mkVar p|]))); tclDO 3 (Proofview.V82.of_tactic intro); @@ -973,17 +958,17 @@ let rec destruct_hex expr_info acc l = match List.rev acc with | [] -> tclIDTAC | (_,p,hp)::tl -> - observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) + observe_tac (fun _ _ -> str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl) end | (v,hex)::l -> - observe_tclTHENLIST (str "destruct_hex")[ + observe_tclTHENLIST (fun _ _ -> str "destruct_hex")[ Proofview.V82.of_tactic (simplest_case (mkVar hex)); Proofview.V82.of_tactic (clear [hex]); tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> observe_tac - (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) + (fun _ _ -> str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) (destruct_hex expr_info ((v,p,hp)::acc) l) ) ) @@ -991,7 +976,7 @@ let rec destruct_hex expr_info acc l = let rec intros_values_eq expr_info acc = tclORELSE( - observe_tclTHENLIST (str "intros_values_eq")[ + observe_tclTHENLIST (fun _ _ -> str "intros_values_eq")[ tclDO 2 (Proofview.V82.of_tactic intro); onNthHypId 1 (fun hex -> (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc))) @@ -1003,16 +988,16 @@ let rec intros_values_eq expr_info acc = let equation_others _ expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch - then - observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) + then + observe_tac (fun env sigma -> str "equation_others (cont_tac +intros) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ pr_leconstr_rd expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ pr_leconstr_rd expr_info.info) (continuation_tac infos) + (observe_tac (fun env sigma -> str "intros_values_eq equation_others " ++ Printer.pr_leconstr_env env sigma expr_info.info) (intros_values_eq expr_info []))) + else observe_tac (fun env sigma -> str "equation_others (cont_tac) " ++ Printer.pr_leconstr_env env sigma expr_info.info) (continuation_tac infos) let equation_app f_and_args expr_info continuation_tac infos = if expr_info.is_final && expr_info.is_main_branch - then ((observe_tac (str "intros_values_eq equation_app") (intros_values_eq expr_info []))) + then ((observe_tac (fun _ _ -> str "intros_values_eq equation_app") (intros_values_eq expr_info []))) else continuation_tac infos let equation_app_rec (f,args) expr_info continuation_tac info g = @@ -1021,19 +1006,19 @@ let equation_app_rec (f,args) expr_info continuation_tac info g = try let v = List.assoc_f (List.equal (EConstr.eq_constr sigma)) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in - observe_tac (str "app_rec found") (continuation_tac new_infos) g + observe_tac (fun _ _ -> str "app_rec found") (continuation_tac new_infos) g with Not_found -> if expr_info.is_final && expr_info.is_main_branch then - observe_tclTHENLIST (str "equation_app_rec") + observe_tclTHENLIST (fun _ _ -> str "equation_app_rec") [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}; - observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info []) + observe_tac (fun _ _ -> str "app_rec intros_values_eq") (intros_values_eq expr_info []) ] g else - observe_tclTHENLIST (str "equation_app_rec1")[ + observe_tclTHENLIST (fun _ _ -> str "equation_app_rec1")[ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args))); - observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) + observe_tac (fun _ _ -> str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc}) ] g end @@ -1070,20 +1055,19 @@ let compute_terminate_type nb_args func = let right = mkRel 5 in let delayed_force c = EConstr.Unsafe.to_constr (delayed_force c) in let equality = mkApp(delayed_force eq, [|lift 5 b; left; right|]) in - let result = (mkProd ((Name def_id) , lift 4 a_arrow_b, equality)) in + let result = (mkProd (make_annot (Name def_id) Sorts.Relevant, lift 4 a_arrow_b, equality)) in let cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in let nb_iter = mkApp(delayed_force ex, [|delayed_force nat; (mkLambda - (Name - p_id, + (make_annot (Name p_id) Sorts.Relevant, delayed_force nat, - (mkProd (Name k_id, delayed_force nat, - mkArrow cond result))))|])in + (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, + mkArrow cond Sorts.Relevant result))))|])in let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), [|b; - (mkLambda (Name v_id, b, nb_iter))|]) in + (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1118,7 +1102,7 @@ let termination_proof_header is_mes input_type ids args_id relation (h_intros args_id) (tclTHENS (observe_tac - (str "first assert") + (fun _ _ -> str "first assert") (Proofview.V82.of_tactic (assert_before (Name wf_rec_arg) (mkApp (delayed_force acc_rel, @@ -1130,7 +1114,7 @@ let termination_proof_header is_mes input_type ids args_id relation (* accesibility proof *) tclTHENS (observe_tac - (str "second assert") + (fun _ _ -> str "second assert") (Proofview.V82.of_tactic (assert_before (Name wf_thm) (mkApp (delayed_force well_founded,[|input_type;relation|])) @@ -1138,26 +1122,26 @@ let termination_proof_header is_mes input_type ids args_id relation ) [ (* interactive proof that the relation is well_founded *) - observe_tac (str "wf_tac") (wf_tac is_mes (Some args_id)); + observe_tac (fun _ _ -> str "wf_tac") (wf_tac is_mes (Some args_id)); (* this gives the accessibility argument *) observe_tac - (str "apply wf_thm") + (fun _ _ -> str "apply wf_thm") (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))) ) ] ; (* rest of the proof *) - observe_tclTHENLIST (str "rest of proof") - [observe_tac (str "generalize") + observe_tclTHENLIST (fun _ _ -> str "rest of proof") + [observe_tac (fun _ _ -> str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id]))) )) ; - observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1))); + observe_tac (fun _ _ -> 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) + observe_tac (fun _ _ -> str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv) ] ] ) g @@ -1181,15 +1165,15 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let func_body = EConstr.of_constr func_body in let (f_name, _, body1) = destLambda sigma func_body in let f_id = - match f_name with + match f_name.binder_name with | Name f_id -> next_ident_away_in_goal f_id ids | Anonymous -> anomaly (Pp.str "Anonymous function.") in let n_names_types,_ = decompose_lam_n sigma nb_args body1 in let n_ids,ids = List.fold_left - (fun (n_ids,ids) (n_name,_) -> - match n_name with + (fun (n_ids,ids) (n_name,_) -> + match n_name.binder_name with | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids @@ -1236,14 +1220,14 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a g end -let get_current_subgoals_types () = - let p = Proof_global.give_me_the_proof () in +let get_current_subgoals_types pstate = + let p = Proof_global.give_me_the_proof pstate in let sgs,_,_,_,sigma = Proof.proof p in sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals let build_and_l sigma l = - let and_constr = UnivGen.constr_of_global @@ Coqlib.lib_ref "core.and.type" 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 @@ -1286,19 +1270,19 @@ let is_rec_res id = let clear_goals sigma = let rec clear_goal t = match EConstr.kind sigma t with - | Prod(Name id as na,t',b) -> + | Prod({binder_name=Name id} as na,t',b) -> let b' = clear_goal b in if noccurn sigma 1 b' && (is_rec_res id) then Vars.lift (-1) b' else if b' == b then t - else mkProd(na,t',b') + else mkProd(na,t',b') | _ -> EConstr.map sigma clear_goal t in List.map clear_goal -let build_new_goal_type () = - let sigma, sub_gls_types = get_current_subgoals_types () in +let build_new_goal_type pstate = + let sigma, sub_gls_types = get_current_subgoals_types pstate in (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sigma sub_gls_types in (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) @@ -1311,21 +1295,22 @@ let is_opaque_constant c = | Declarations.OpaqueDef _ -> Proof_global.Opaque | Declarations.Undef _ -> Proof_global.Opaque | Declarations.Def _ -> Proof_global.Transparent + | Declarations.Primitive _ -> Proof_global.Opaque -let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = +let open_new_goal pstate 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); *) - let current_proof_name = Proof_global.get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name pstate in let name = match goal_name with | Some s -> s | 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 hook _ _ _ _ = let opacity = let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in @@ -1338,11 +1323,10 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in - Proof_global.discard_all (); - build_proof (Evd.from_env env) + let pstate = build_proof env (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in - observe_tclTHENLIST (str "") + observe_tclTHENLIST (fun _ _ -> str "") [ Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); @@ -1366,7 +1350,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g | _ -> incr h_num; - (observe_tac (str "finishing using") + (observe_tac (fun _ _ -> str "finishing using") ( tclCOMPLETE( tclFIRST[ @@ -1376,26 +1360,25 @@ 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] ] ) ) ) g) -; - Lemmas.save_proof (Vernacexpr.Proved(opacity,None)); + in + let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in + () in - Lemmas.start_proof + let pstate = Lemmas.start_proof ~ontop:(Some pstate) na (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma) - sigma gls_type - (Lemmas.mk_hook hook); - if Indfun_common.is_strict_tcc () + sigma gls_type ~hook:(Lemmas.mk_hook hook) in + let pstate = if Indfun_common.is_strict_tcc () then - ignore (by (Proofview.V82.tactic (tclIDTAC))) + fst @@ by (Proofview.V82.tactic (tclIDTAC)) pstate else - begin - ignore (by (Proofview.V82.tactic begin + fst @@ by (Proofview.V82.tactic begin fun g -> tclTHEN (decompose_and_tac) @@ -1411,14 +1394,12 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ) using_lemmas) ) tclIDTAC) - g end)) - end; + g end) pstate + in try - ignore (by (Proofview.V82.tactic tclIDTAC)); (* raises UserError _ if the proof is complete *) + Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *) with UserError _ -> - defined () - - + defined pstate let com_terminate tcc_lemma_name @@ -1431,32 +1412,26 @@ let com_terminate thm_name using_lemmas nb_args ctx hook = - let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evd, env = Pfedit.get_current_context () in - Lemmas.start_proof thm_name + let start_proof env ctx (tac_start:tactic) (tac_end:tactic) = + let pstate = Lemmas.start_proof ~ontop:None thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; - - ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start))); - ignore (by (Proofview.V82.tactic (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref - input_type relation rec_arg_num )))) + ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in + let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in + fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref + input_type relation rec_arg_num ))) pstate in - start_proof ctx tclIDTAC tclIDTAC; + let pstate = start_proof Global.(env ()) ctx tclIDTAC tclIDTAC in try - let sigma, new_goal_type = build_new_goal_type () in + let sigma, new_goal_type = build_new_goal_type pstate in let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in - open_new_goal start_proof sigma + open_new_goal pstate start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) - (new_goal_type); + (new_goal_type) with EmptySubgoals -> (* a non recursive function declared with measure ! *) tcc_lemma_ref := Not_needed; - defined () - - - - + defined pstate let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = @@ -1466,34 +1441,27 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) let terminate_constr = EConstr.of_constr terminate_constr in let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in - observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ + observe_tac (fun _ _ -> str "start_equation") (observe_tclTHENLIST (fun _ _ -> str "start_equation") [ h_intros x; Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]); - observe_tac (str "simplest_case") + observe_tac (fun _ _ -> str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); - observe_tac (str "prove_eq") (cont_tactic x)]) g;; + observe_tac (fun _ _ -> str "prove_eq") (cont_tactic x)]) g;; -let (com_eqn : int -> Id.t -> - GlobRef.t -> GlobRef.t -> GlobRef.t - -> Constr.t -> unit) = - fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> +let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type = let open CVars in let opacity = match terminate_ref with | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evd, env = Pfedit.get_current_context () in - let evd = Evd.from_ctx (Evd.evar_universe_context evd) in + let evd = Evd.from_ctx uctx in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in - (Lemmas.start_proof eq_name (Global, false, Proof Lemma) - ~sign:(Environ.named_context_val env) - evd - (EConstr.of_constr equation_lemma_type) - (Lemmas.mk_hook (fun _ _ -> ())); - ignore (by + let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd + (EConstr.of_constr equation_lemma_type) in + let pstate = fst @@ by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) @@ -1520,40 +1488,42 @@ let (com_eqn : int -> Id.t -> ih = Id.of_string "______"; } ) - ))); + )) pstate in (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *) (* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *) - Flags.silently (fun () -> Lemmas.save_proof (Vernacexpr.Proved(opacity,None))) () ; -(* Pp.msgnl (str "eqn finished"); *) - );; + let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in + () +(* Pp.msgnl (fun _ _ -> str "eqn finished"); *) + let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq - generate_induction_principle using_lemmas : unit = + generate_induction_principle using_lemmas : Proof_global.t option = let open Term in let open Constr in let open CVars in 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 env = EConstr.push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in + let evd, function_type = interp_type_evars ~program_mode:false env evd type_of_f in + let function_r = Sorts.Relevant in (* TODO relevance *) + let env = EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot function_name function_r,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 evd, ty = interp_type_evars ~program_mode:false env evd ~impls:rec_impls eq in let evd = Evd.minimize_universes evd in - let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) 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 ()); *) + (* Pp.msgnl (fun _ _ -> 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'); *) -(* Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *) -(* Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *) +(* Pp.msgnl (fun _ _ -> str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *) +(* Pp.msgnl (fun _ _ -> str "rec_arg_num := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *) +(* Pp.msgnl (fun _ _ -> str "eq' := " ++ str (fun _ _ -> string_of_int rec_arg_num)); *) match Constr.kind eq' with | App(e,[|_;_;eq_fix|]) -> - mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars eq_fix)) + mkLambda (make_annot (Name function_name) Sorts.Relevant,function_type,subst_var function_name (compose_lam res_vars eq_fix)) | _ -> failwith "Recursive Definition (res not eq)" in let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in @@ -1563,7 +1533,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + let univs = Evd.univ_entry ~poly:false evd in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) @@ -1575,14 +1545,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in - (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) - let hook _ _ = + (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) + let hook uctx _ _ _ = 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 [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); + let stop = + (* XXX: What is the correct way to get sign at hook time *) + let sign = Environ.named_context_val Global.(env ()) in + try com_eqn sign uctx (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); false with e when CErrors.noncritical e -> begin @@ -1614,14 +1586,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num in (* XXX STATE Why do we need this... why is the toplevel protection not enought *) funind_purify (fun () -> - com_terminate - tcc_lemma_name - tcc_lemma_constr - is_mes functional_ref - (EConstr.of_constr rec_arg_type) - relation rec_arg_num - term_id - using_lemmas - (List.length res_vars) - evd (Lemmas.mk_hook hook)) - () + let pstate = com_terminate + tcc_lemma_name + tcc_lemma_constr + is_mes functional_ref + (EConstr.of_constr rec_arg_type) + relation rec_arg_num + term_id + using_lemmas + (List.length res_vars) + evd (Lemmas.mk_hook hook) + in pstate) () diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli index 549f1fc0e4..a006c2c354 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 -> unit) -> Constrexpr.constr_expr list -> unit + pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option |