diff options
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 473 |
1 files changed, 263 insertions, 210 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index fa84e4dd..fb9ae64b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1,12 +1,18 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Term + +module CVars = Vars + +open Constr +open EConstr open Vars open Namegen open Environ @@ -25,7 +31,7 @@ open Nametab open Declare open Decl_kinds open Tacred -open Proof_type +open Goal open Pfedit open Glob_term open Pretyping @@ -39,56 +45,63 @@ open Auto open Eauto open Indfun_common -open Sigma.Notations open Context.Rel.Declaration - (* Ugly things which should not be here *) -let coq_constant m s = - Coqlib.coq_constant "RecursiveDefinition" m s +let coq_constant m s = EConstr.of_constr @@ Universes.constr_of_global @@ + Coqlib.coq_reference "RecursiveDefinition" m s let arith_Nat = ["Arith";"PeanoNat";"Nat"] let arith_Lt = ["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 = - Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s + EConstr.of_constr ( + Universes.constr_of_global @@ + Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s) let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in locate (make_qualid dp (Id.of_string s)) -let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = - let ce = definition_entry ~univs:ctx value (*FIXME *) in +let declare_fun f_id kind ?univs value = + let ce = definition_entry ?univs value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = - match (kind_of_term t) with + match (Constr.kind t) with Const sp -> (try (match constant_opt_value_in (Global.env ()) sp with | Some c -> c | _ -> raise Not_found) with Not_found -> anomaly (str "Cannot find definition of constant " ++ - (Id.print (Label.to_id (con_label (fst sp))))) + (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".") ) |_ -> assert false -let type_of_const t = - match (kind_of_term t) with - Const sp -> Typeops.type_of_constant (Global.env()) sp +let type_of_const sigma t = + match (EConstr.kind sigma t) with + | Const (sp, u) -> + let u = EInstance.kind sigma u in + (* FIXME discarding universe constraints *) + Typeops.type_of_constant_in (Global.env()) (sp, u) |_ -> assert false let constr_of_global x = - fst (Universes.unsafe_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 const_of_ref = function ConstRef kn -> kn - | _ -> anomaly (Pp.str "ConstRef expected") + | _ -> anomaly (Pp.str "ConstRef expected.") let nf_zeta env = @@ -98,9 +111,7 @@ let nf_zeta env = let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *) - let clos_norm_flags flgs env sigma t = - CClosure.norm_val (CClosure.create_clos_infos flgs env) (CClosure.inject (Reductionops.nf_evar sigma t)) in - clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty + Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty @@ -110,13 +121,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in + let ids = Id.Set.of_list ids in List.fold_right - (fun id acc -> next_global_ident_away id (acc@ids)::acc) + (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc) idl [] +let next_ident_away_in_goal ids avoid = + next_ident_away_in_goal ids (Id.Set.of_list avoid) + let compute_renamed_type gls c = - rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) [] + rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" @@ -128,13 +143,13 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" - with Not_found -> error "module Recdef not loaded" -let iter = function () -> (constr_of_global (delayed_force iter_ref)) + with Not_found -> user_err Pp.(str "module Recdef not loaded") +let iter_rd = function () -> (constr_of_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") @@ -147,7 +162,7 @@ let coq_O = function () -> (coq_init_constant "O") let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") -let max_constr = function () -> (constr_of_global (delayed_force max_ref)) +let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -166,9 +181,10 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f:constr list -> global_reference -> constr) = +let (value_f: Constr.t list -> global_reference -> Constr.t) = + let open Term in + let open Constr in fun al fterm -> - let d0 = Loc.ghost in let rev_x_id_l = ( List.fold_left @@ -185,21 +201,21 @@ let (value_f:constr list -> global_reference -> constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - GCases - (d0,RegularStyle,None, - [GApp(d0, GRef(d0,fterm,None), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l), + DAst.make @@ + GCases + (RegularStyle,None, + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [d0, [v_id], [PatCstr(d0,(destIndRef - (delayed_force coq_sig_ref),1), - [PatVar(d0, Name v_id); - PatVar(d0, Anonymous)], - Anonymous)], - GVar(d0,v_id)]) + [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], + Anonymous)], + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in + let body = EConstr.Unsafe.to_constr body in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Constr.t list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -301,14 +317,14 @@ 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 forbidden e = +let check_not_nested sigma forbidden e = let rec check_not_nested e = - match kind_of_term e with + match EConstr.kind sigma e with | Rel _ -> () | Var x -> if Id.List.mem x forbidden - then errorlabstrm "Recdef.check_not_nested" - (str "check_not_nested: failure " ++ pr_id x) + then user_err ~hdr:"Recdef.check_not_nested" + (str "check_not_nested: failure " ++ Id.print x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -321,13 +337,14 @@ let check_not_nested forbidden e = | Construct _ -> () | Case(_,t,e,a) -> check_not_nested t;check_not_nested e;Array.iter check_not_nested a - | Fix _ -> error "check_not_nested : Fix" - | CoFix _ -> error "check_not_nested : Fix" + | Fix _ -> user_err Pp.(str "check_not_nested : Fix") + | CoFix _ -> user_err Pp.(str "check_not_nested : Fix") in try check_not_nested e with UserError(_,p) -> - errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ 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 *) type 'a infos = @@ -374,15 +391,17 @@ type journey_info = -let rec add_vars forbidden e = - match kind_of_term e with +let add_vars sigma forbidden e = + let rec aux forbidden e = + match EConstr.kind sigma e with | Var x -> x::forbidden - | _ -> fold_constr add_vars forbidden e - + | _ -> EConstr.fold sigma aux forbidden e + in + aux 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 nb_lam e in + let rev_context,b = decompose_lam_n (project g) nb_lam e in let ids = List.fold_left (fun acc (na,_) -> let pre_id = match na with @@ -404,17 +423,17 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = (fun g' -> let ty_teq = pf_unsafe_type_of g' (mkVar heq) in let teq_lhs,teq_rhs = - let _,args = try destApp ty_teq with DestKO -> assert false in + let _,args = try destApp (project g') ty_teq with DestKO -> assert false in args.(1),args.(2) in - let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in + let new_b' = Termops.replace_term (project g') teq_lhs teq_rhs new_b in let new_infos = { infos with info = new_b'; eqs = heq::infos.eqs; forbidden_ids = if forbid_new_ids - then add_vars infos.forbidden_ids new_b' + then add_vars (project g') infos.forbidden_ids new_b' else infos.forbidden_ids } in finalize_tac new_infos g' @@ -423,34 +442,35 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = ) ] g -let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = - match kind_of_term expr_info.info with - | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint" - | Proj _ -> error "Function cannot treat projections" +let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = + let sigma = project 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) -> begin let new_continuation_tac = jinfo.letiN (na,b,t,e) expr_info continuation_tac in travel jinfo new_continuation_tac - {expr_info with info = b; is_final=false} + {expr_info with info = b; is_final=false} g end - | Rel _ -> anomaly (Pp.str "Free var in goal conclusion !") + | Rel _ -> anomaly (Pp.str "Free var in goal conclusion!") | Prod _ -> begin try - check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info + check_not_nested 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 -> - errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + 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) end | Lambda(n,t,b) -> begin try - check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; - jinfo.otherS () expr_info continuation_tac expr_info + check_not_nested 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 -> - errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + 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) end | Case(ci,t,a,l) -> begin @@ -461,15 +481,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = travel jinfo continuation_tac_a {expr_info with info = a; is_main_branch = false; - is_final = false} + is_final = false} g end | App _ -> - let f,args = decompose_app expr_info.info in - if eq_constr f (expr_info.f_constr) - then jinfo.app_reC (f,args) expr_info continuation_tac expr_info + let f,args = decompose_app sigma expr_info.info in + if EConstr.eq_constr sigma f (expr_info.f_constr) + then jinfo.app_reC (f,args) expr_info continuation_tac expr_info g else begin - match kind_of_term f with + match EConstr.kind sigma f with | App _ -> assert false (* f is coming from a decompose_app *) | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ | Sort _ | Prod _ | Var _ -> @@ -477,15 +497,15 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = let new_continuation_tac = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo - expr_info.is_main_branch new_continuation_tac new_infos - | Case _ -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr 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_lconstr expr_info.info) + 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 ".") end - | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} + | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} g | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> let new_continuation_tac = jinfo.otherS () expr_info continuation_tac in - new_continuation_tac expr_info + new_continuation_tac expr_info g and travel_args jinfo is_final continuation_tac infos = let (f_args',args) = infos.info in match args with @@ -502,27 +522,28 @@ and travel_args jinfo is_final continuation_tac infos = {infos with info=arg;is_final=false} and travel jinfo continuation_tac expr_info = observe_tac - (str jinfo.message ++ Printer.pr_lconstr expr_info.info) + (str jinfo.message ++ pr_leconstr_rd expr_info.info) (travel_aux jinfo continuation_tac expr_info) (* Termination proof *) let rec prove_lt hyple g = + let sigma = project g in begin try - let (varx,varz) = match decompose_app (pf_concl g) with - | _, x::z::_ when isVar x && isVar z -> x, z + let (varx,varz) = match decompose_app sigma (pf_concl g) with + | _, x::z::_ when isVar sigma x && isVar sigma z -> x, z | _ -> assert false in let h = List.find (fun id -> - match decompose_app (pf_unsafe_type_of g (mkVar id)) with - | _, t::_ -> eq_constr t varx + match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with + | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in observe_tclTHENLIST (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) @@ -638,12 +659,13 @@ let terminate_others _ expr_info continuation_tac infos = ] else continuation_tac infos -let terminate_letin (na,b,t,e) expr_info continuation_tac info = +let terminate_letin (na,b,t,e) expr_info continuation_tac info g = + let sigma = project g in let new_e = subst1 info.info e in let new_forbidden = let forbid = try - check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b; + check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) b; true with e when CErrors.noncritical e -> false in @@ -654,7 +676,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info = | Name id -> id::info.forbidden_ids else info.forbidden_ids in - continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} + continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g let pf_type c tac gl = let evars, ty = Typing.type_of (pf_env gl) (project gl) c in @@ -673,7 +695,7 @@ let pf_typel l tac = introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) let mkDestructEq : - Id.t list -> constr -> goal sigma -> tactic * Id.t list = + Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list = fun not_on_hyp expr g -> let hyps = pf_hyps g in let to_revert = @@ -681,7 +703,7 @@ let mkDestructEq : (fun decl -> let open Context.Named.Declaration in let id = get_id decl in - if Id.List.mem id not_on_hyp || not (Termops.occur_term expr (get_type decl)) + if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in @@ -691,18 +713,18 @@ let mkDestructEq : observe_tclTHENLIST (str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); (fun g2 -> - let changefun patvars = { run = fun sigma -> - let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in - redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2) - } in + let changefun patvars sigma = + pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) + in Proofview.V82.of_tactic (change_in_concl None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = + let sigma = project g in let f_is_present = try - check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a; + check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) a; false with e when CErrors.noncritical e -> true @@ -716,25 +738,26 @@ 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_lconstr a') + observe_tac (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) )) with - | UserError("Refiner.thensn_tac3",_) - | UserError("Refiner.tclFAIL_s",_) -> - (observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} ) + | 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} ) )) g -let terminate_app_rec (f,args) expr_info continuation_tac _ = - List.iter (check_not_nested (expr_info.f_id::expr_info.forbidden_ids)) +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)) args; begin try - let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in + 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")[ continuation_tac new_infos; @@ -748,7 +771,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = ] else tclIDTAC - ] + ] g with Not_found -> observe_tac (str "terminate_app_rec not found") (tclTHENS (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))) @@ -805,7 +828,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = ); ] ]) - ]) + ]) g end let terminate_info = @@ -827,8 +850,9 @@ 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) let rec prove_le g = + let sigma = project g in let x,z = - let _,args = decompose_app (pf_concl g) in + let _,args = decompose_app sigma (pf_concl g) in (List.hd args,List.hd (List.tl args)) in tclFIRST[ @@ -836,13 +860,17 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (reference_of_constr (le ())),[|Pattern.PVar (destVar x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + EConstr.is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = - let _,args = decompose_app t in + let _,args = decompose_app sigma t in List.hd (List.tl args) in observe_tclTHENLIST (str "prove_le")[ @@ -858,21 +886,21 @@ 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 " ++ pr_id p ) ( + (observe_tac (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 t_eq in - let _,_,t = destProd t in - let def_na,_,_ = destProd t in - Nameops.out_name k_na,Nameops.out_name 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,Nameops.Name.get_id def_na in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S max)]) false) g) ) + ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr); + 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 *) @@ -886,20 +914,20 @@ let make_rewrite expr_info l hp max = (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l)) (observe_tac (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 t_eq in - let _,_,t = destProd t in - let def_na,_,_ = destProd t in - Nameops.out_name k_na,Nameops.out_name 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,Nameops.Name.get_id def_na in observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true (mkVar hp, - ExplicitBindings[Loc.ghost,NamedHyp def, - expr_info.f_constr;Loc.ghost,NamedHyp k, - (f_S (f_S max))]) false)) g) + 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") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ @@ -916,7 +944,7 @@ let make_rewrite expr_info l hp max = ])) ; observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *) - Proofview.V82.of_tactic (apply (delayed_force le_lt_SS)); + Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS))); observe_tac (str "prove_le (3)") prove_le ] ]) @@ -953,7 +981,7 @@ let rec destruct_hex expr_info acc l = onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> observe_tac - (str "destruct_hex after " ++ pr_id hp ++ spc () ++ pr_id p) + (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) (destruct_hex expr_info ((v,p,hp)::acc) l) ) ) @@ -974,23 +1002,24 @@ 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) " ++ Printer.pr_lconstr expr_info.info) + observe_tac (str "equation_others (cont_tac +intros) " ++ pr_leconstr_rd expr_info.info) (tclTHEN (continuation_tac infos) - (observe_tac (str "intros_values_eq equation_others " ++ Printer.pr_lconstr expr_info.info) (intros_values_eq expr_info []))) - else observe_tac (str "equation_others (cont_tac) " ++ Printer.pr_lconstr expr_info.info) (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) 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 []))) else continuation_tac infos -let equation_app_rec (f,args) expr_info continuation_tac info = +let equation_app_rec (f,args) expr_info continuation_tac info g = + let sigma = project g in begin try - let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in + 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) + observe_tac (str "app_rec found") (continuation_tac new_infos) g with Not_found -> if expr_info.is_final && expr_info.is_main_branch then @@ -998,12 +1027,12 @@ let equation_app_rec (f,args) expr_info continuation_tac info = [ 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 []) - ] + ] g else observe_tclTHENLIST (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}) - ] + ] g end let equation_info = @@ -1022,10 +1051,13 @@ let prove_eq = travel equation_info (* [compute_terminate_type] computes the type of the Definition f_terminate from the type of f_F *) let compute_terminate_type nb_args func = + let open Term in + let open Constr in + let open CVars in let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = - mkApp(delayed_force iter, + mkApp(delayed_force iter_rd, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: constr_of_global func::mkRel 1:: @@ -1034,6 +1066,7 @@ let compute_terminate_type nb_args func = ) in 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 cond = mkApp(delayed_force lt, [|(mkRel 2); (mkRel 1)|]) in @@ -1046,7 +1079,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (Name k_id, delayed_force nat, mkArrow cond result))))|])in - let value = mkApp(constr_of_global (delayed_force coq_sig_ref), + let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), [|b; (mkLambda (Name v_id, b, nb_iter))|]) in compose_prod rev_args value @@ -1130,25 +1163,27 @@ let termination_proof_header is_mes input_type ids args_id relation -let rec instantiate_lambda t l = +let rec instantiate_lambda sigma t l = match l with | [] -> t | a::l -> - let (_, _, body) = destLambda t in - instantiate_lambda (subst1 a body) l + let (_, _, body) = destLambda sigma t in + instantiate_lambda sigma (subst1 a body) l let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic = begin fun g -> + let sigma = project g in let ids = Termops.ids_of_named_context (pf_hyps g) in let func_body = (def_of_const (constr_of_global func)) in - let (f_name, _, body1) = destLambda func_body in + 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 | Name f_id -> next_ident_away_in_goal f_id ids - | Anonymous -> anomaly (Pp.str "Anonymous function") + | Anonymous -> anomaly (Pp.str "Anonymous function.") in - let n_names_types,_ = decompose_lam_n nb_args body1 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,_) -> @@ -1156,13 +1191,13 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a | Name id -> let n_id = next_ident_away_in_goal id ids in n_id::n_ids,n_id::ids - | _ -> anomaly (Pp.str "anonymous argument") + | _ -> anomaly (Pp.str "anonymous argument.") ) ([],(f_id::ids)) n_names_types in let rec_arg_id = List.nth n_ids (rec_arg_num - 1) in - let expr = instantiate_lambda func_body (mkVar f_id::(List.map mkVar n_ids)) in + let expr = instantiate_lambda sigma func_body (mkVar f_id::(List.map mkVar n_ids)) in termination_proof_header is_mes input_type @@ -1201,20 +1236,21 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types () = let p = Proof_global.give_me_the_proof () in - let { Evd.it=sgs ; sigma=sigma } = Proof.V82.subgoals p in - sigma, List.map (Goal.V82.abstract_type sigma) sgs + let sgs,_,_,_,sigma = Proof.proof p in + sigma, List.map (Goal.V82.abstract_type sigma) sgs -let build_and_l l = - let and_constr = Coqlib.build_coq_and () in +exception EmptySubgoals +let build_and_l sigma l = + let and_constr = Universes.constr_of_global @@ Coqlib.build_coq_and () in let conj_constr = coq_conj () in let mk_and p1 p2 = - Term.mkApp(and_constr,[|p1;p2|]) in + mkApp(EConstr.of_constr and_constr,[|p1;p2|]) in let rec is_well_founded t = - match kind_of_term t with + match EConstr.kind sigma t with | Prod(_,_,t') -> is_well_founded t' | App(_,_) -> - let (f,_) = decompose_app t in - eq_constr f (well_founded ()) + let (f,_) = decompose_app sigma t in + EConstr.eq_constr sigma f (well_founded ()) | _ -> false in @@ -1225,13 +1261,13 @@ let build_and_l l = in let l = List.sort compare l in let rec f = function - | [] -> failwith "empty list of subgoals!" + | [] -> raise EmptySubgoals | [p] -> p,tclIDTAC,1 | p1::pl -> let c,tac,nb = f pl in mk_and p1 c, tclTHENS - (Proofview.V82.of_tactic (apply (constr_of_global conj_constr))) + (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr)))) [tclIDTAC; tac ],nb+1 @@ -1245,16 +1281,16 @@ let is_rec_res id = String.equal (String.sub id_name 0 (String.length rec_res_name)) rec_res_name with Invalid_argument _ -> false -let clear_goals = +let clear_goals sigma = let rec clear_goal t = - match kind_of_term t with + match EConstr.kind sigma t with | Prod(Name id as na,t',b) -> let b' = clear_goal b in - if noccurn 1 b' && (is_rec_res id) - then Termops.pop b' + 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') - | _ -> Term.map_constr clear_goal t + | _ -> EConstr.map sigma clear_goal t in List.map clear_goal @@ -1262,41 +1298,41 @@ let clear_goals = let build_new_goal_type () = let sigma, sub_gls_types = get_current_subgoals_types () 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 sub_gls_types in + 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); *) - let res = build_and_l sub_gls_types in + let res = build_and_l sigma sub_gls_types in sigma, res let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None - | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque + | Declarations.Undef _ -> Vernacexpr.Opaque | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) - let current_proof_name = get_current_proof_name () in + let current_proof_name = Proof_global.get_current_proof_name () 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 unamed theorem.") in - let na = next_global_ident_away name [] in - if Termops.occur_existential gls_type then - CErrors.error "\"abstract\" cannot handle existentials"; + let na = next_global_ident_away name Id.Set.empty in + if Termops.occur_existential sigma gls_type then + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = Libnames.Ident (Loc.ghost,na) in + let na_ref = CAst.make @@ Libnames.Ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c - | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant") + | _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant.") in let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in - ref_ := Some lemma ; + ref_ := Value (EConstr.Unsafe.to_constr lemma); let lid = ref [] in let h_num = ref (-1) in let env = Global.env () in @@ -1322,8 +1358,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ); ] gls) (fun g -> - match kind_of_term (pf_concl g) with - | App(f,_) when eq_constr f (well_founded ()) -> + let sigma = project g in + match EConstr.kind sigma (pf_concl g) with + | App(f,_) when EConstr.eq_constr sigma f (well_founded ()) -> Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g | _ -> incr h_num; @@ -1336,7 +1373,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (Proofview.V82.of_tactic e_assumption); Eauto.eauto_with_bases (true,5) - [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] + [(fun _ sigma -> (sigma, (Lazy.force refl_equal)))] [Hints.Hint_db.empty empty_transparent_state false] ] ) @@ -1366,7 +1403,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp (fun c -> Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST [intros; - Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); + Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*); Tacticals.New.tclCOMPLETE Auto.default_auto ]) ) @@ -1393,10 +1430,10 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let (evmap, env) = Lemmas.get_current_context() in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) - ctx (compute_terminate_type nb_args fonctional_ref) hook; + 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 @@ -1410,8 +1447,9 @@ let com_terminate using_lemmas tcc_lemma_ref (Some tcc_lemma_name) (new_goal_type); - with Failure "empty list of subgoals!" -> + with EmptySubgoals -> (* a non recursive function declared with measure ! *) + tcc_lemma_ref := Not_needed; defined () @@ -1420,9 +1458,11 @@ let com_terminate let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:Id.t list -> tactic) g = + let sigma = project g in let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in + 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") [ h_intros x; @@ -1434,34 +1474,35 @@ let start_equation (f:global_reference) (term_f:global_reference) let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference - -> constr -> unit) = + -> Constr.t -> unit) = fun 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") + | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let (evmap, env) = Lemmas.get_current_context() in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) 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) - evmap - equation_lemma_type + evd + (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by (Proofview.V82.tactic (start_equation f_ref terminate_ref (fun x -> prove_eq (fun _ -> tclIDTAC) {nb_arg=nb_arg; - f_terminate = constr_of_global terminate_ref; - f_constr = f_constr; + f_terminate = EConstr.of_constr (constr_of_global terminate_ref); + f_constr = EConstr.of_constr f_constr; concl_tac = tclIDTAC; func=functional_ref; - info=(instantiate_lambda - (def_of_const (constr_of_global functional_ref)) - (f_constr::List.map mkVar x) + info=(instantiate_lambda Evd.empty + (EConstr.of_constr (def_of_const (constr_of_global functional_ref))) + (EConstr.of_constr f_constr::List.map mkVar x) ); is_main_branch = true; is_final = true; @@ -1484,27 +1525,33 @@ let (com_eqn : int -> Id.t -> (* Pp.msgnl (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 = + let open Term in + let open Constr in + let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in + let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in - let evm, nf = Evarutil.nf_evars_and_universes !evd in - let equation_lemma_type = nf_betaiotazeta (nf ty) in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in + let ty = EConstr.Unsafe.to_constr ty in + let evd, nf = Evarutil.nf_evars_and_universes evd in + let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in + let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *) let res_vars,eq' = decompose_prod equation_lemma_type in let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in - let eq' = nf_zeta env_eq' eq' in + let eq' = nf_zeta env_eq' (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)); *) - match kind_of_term eq' with + 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)) | _ -> failwith "Recursive Definition (res not eq)" @@ -1515,21 +1562,24 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + let functional_ref = + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res + in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in - let tcc_lemma_constr = ref None 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 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 [Ident (Loc.ghost,term_id)] in + let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ 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); @@ -1538,7 +1588,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num begin if do_observe () then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) - else CErrors.errorlabstrm "Cannot create equation Lemma" + else CErrors.user_err ~hdr:"Cannot create equation Lemma" (str "Cannot create equation lemma." ++ spc () ++ str "This may be because the function is nested-recursive.") ; @@ -1552,23 +1602,26 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation; - if Flags.is_verbose () - then msgnl (h 1 (Ppconstr.pr_id function_name ++ + functional_ref eq_ref rec_arg_num + (EConstr.of_constr rec_arg_type) + (nb_prod evd (EConstr.of_constr res)) relation; + Flags.if_verbose + msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ h 1 (Ppconstr.pr_id equation_id ++ spc () ++ str"is defined" ) ) in - States.with_state_protection_on_exception (fun () -> + (* 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 - rec_arg_type + (EConstr.of_constr rec_arg_type) relation rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () |