diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 58 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 19 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 21 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 32 |
8 files changed, 76 insertions, 76 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6db0a1119b..9749af1e66 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -475,7 +475,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = tclIDTAC in try - scan_type [] (Typing.unsafe_type_of env sigma (mkVar hyp_id)), [hyp_id] + scan_type [] (Typing.type_of_variable env hyp_id), [hyp_id] with TOREMOVE -> thin [hyp_id],[] @@ -525,7 +525,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps; observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) - let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in + let new_term_value_eq = pf_get_hyp_typ g' heq_id in (* compute the new value of the body *) let new_term_value = match EConstr.kind (project g') new_term_value_eq with @@ -536,22 +536,23 @@ 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(make_annot Anonymous Sorts.Relevant, - pf_unsafe_type_of g' term, - Termops.replace_term (project g') term (mkRel 1) dyn_infos.info - ) - in - let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in - let new_infos = - {dyn_infos with + let g', termtyp = tac_type_of g' term in + let fun_body = + mkLambda(make_annot Anonymous Sorts.Relevant, + termtyp, + Termops.replace_term (project g') term (mkRel 1) dyn_infos.info + ) + in + let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in + let new_infos = + {dyn_infos with info = new_body; eq_hyps = heq_id::dyn_infos.eq_hyps - } - in - clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) - ] + } + in + clean_goal_with_heq ptes_infos continue_tac new_infos g' + )]) + ] g @@ -633,7 +634,7 @@ let build_proof let dyn_infos = {dyn_info' with info = mkCase(ci,ct,t,cb)} in let g_nb_prod = nb_prod (project g) (pf_concl g) in - let type_of_term = pf_unsafe_type_of g t in + let g, type_of_term = tac_type_of g t in let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in @@ -849,7 +850,7 @@ let generalize_non_dep hyp g = (* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *) let hyps = [hyp] in let env = Global.env () in - let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in + let hyp_typ = pf_get_hyp_typ g hyp in let to_revert,_ = let open Context.Named.Declaration in Environ.fold_named_context_reverse (fun (clear,keep) decl -> @@ -1351,7 +1352,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic = let rewrite = tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs ) in - let _,hrec_concl = decompose_prod (project gls) (pf_unsafe_type_of gls (mkVar hrec)) in + let _,hrec_concl = decompose_prod (project gls) (pf_get_hyp_typ gls hrec) in let f_app = Array.last (snd (destApp (project gls) hrec_concl)) in let f = (fst (destApp (project gls) f_app)) in let rec backtrack : tactic = @@ -1573,19 +1574,16 @@ let prove_principle_for_gen (List.rev_map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - (* observe_tac "" *) Proofview.V82.of_tactic (assert_by - (Name acc_rec_arg_id) - (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) - (Proofview.V82.tactic prove_rec_arg_acc) - ); -(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) -(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *) - (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); -(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *) + Proofview.V82.of_tactic + (assert_by + (Name acc_rec_arg_id) + (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) + (Proofview.V82.tactic prove_rec_arg_acc)); + (revert (List.rev (acc_rec_arg_id::args_ids))); + (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1))); h_intros (List.rev (acc_rec_arg_id::args_ids)); Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref)); - (* observe_tac "finish" *) (fun gl' -> + (fun gl' -> let body = let _,args = destApp (project gl') (pf_concl gl') in Array.last args diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 58efee1518..68661174ac 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -617,7 +617,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i let constructor_args g = List.fold_right (fun hid acc -> - let type_of_hid = pf_unsafe_type_of g (mkVar hid) in + let type_of_hid = pf_get_hyp_typ g hid in let sigma = project g in match EConstr.kind sigma type_of_hid with | Prod(_,_,t') -> @@ -953,7 +953,7 @@ let rec reflexivity_with_destruct_cases g = match sc with None -> tclIDTAC g | Some id -> - match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with + match EConstr.kind (project g) (pf_get_hyp_typ g id) with | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g @@ -993,7 +993,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti (* We get the constant and the principle corresponding to this lemma *) let f = funcs.(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 g, princ_type = tac_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 and compute a fresh name for each of them @@ -1210,7 +1210,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef in let _ = evd := sigma in let l_schemes = - List.map (EConstr.of_constr %> Typing.unsafe_type_of env sigma %> EConstr.Unsafe.to_constr) schemes + List.map (EConstr.of_constr %> Retyping.get_type_of env sigma %> EConstr.Unsafe.to_constr) schemes in let i = ref (-1) in let sorts = @@ -2051,7 +2051,7 @@ let build_case_scheme fa = let (sigma, scheme) = Indrec.build_case_analysis_scheme_default env sigma ind sf in - let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in + let scheme_type = EConstr.Unsafe.to_constr ((Retyping.get_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> fst @@ UnivGen.fresh_sort_in_family x diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e41b92d4dc..84f09c385f 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -514,8 +514,9 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) + (* XXX here and other [understand] calls drop the ctx *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in - let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) rt_as_constr in + let rt_typ = Retyping.get_type_of env (Evd.from_env env) rt_as_constr in let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in @@ -629,7 +630,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret 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 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_type = Retyping.get_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 @@ -646,7 +647,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret 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 + let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -678,7 +679,7 @@ let rec build_entry_lc env sigma funnames avoid rt : glob_constr build_entry_ret nal in 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 + let b_typ = Retyping.get_type_of env (Evd.from_env env) b_as_constr in let (ind,_) = try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> @@ -723,7 +724,7 @@ and build_entry_lc_from_case env sigma funname make_discr let types = List.map (fun (case_arg,_) -> let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in - EConstr.Unsafe.to_constr (Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr) + EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) case_arg_as_constr) ) el in (****** The next works only if the match is not dependent ****) @@ -769,9 +770,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to let env_with_pat_ids = add_pat_variables sigma pat typ new_env in List.fold_right (fun id acc -> - let typ_of_id = - Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) - in + let typ_of_id = Typing.type_of_variable env_with_pat_ids id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id @@ -832,7 +831,7 @@ and build_entry_lc_from_case_term env sigma types funname make_discr patterns_to (fun id acc -> if Id.Set.mem id this_pat_ids then (Prod (Name id), - let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in + let typ_of_id = Typing.type_of_variable new_env id in let raw_typ_of_id = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in @@ -1166,7 +1165,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in let evd = Evd.from_ctx ctx in - let type_t' = Typing.unsafe_type_of env evd t' in + let type_t' = Retyping.get_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 (make_annot n Sorts.Relevant,t',type_t')) env in diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index a205c0744a..f28e98dcc2 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -64,12 +64,10 @@ let functional_induction with_clean c princl pat = | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma in - let princ = (* then we get the principle *) + let sigma, princ = (* then we get the principle *) match princ_option with | Some princ -> - let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT princ + Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) | None -> (*i If there is not default lemma defined then, we cross our finger and try to find a lemma named f_ind @@ -87,19 +85,18 @@ let functional_induction with_clean c princl pat = user_err (str "Cannot find induction principle for " ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') ) in - let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT princ + Evd.fresh_global (pf_env gl) (project gl) princ_ref in - princ >>= fun princ -> - (* We need to refresh gl due to the updated evar_map in princ *) - Proofview.Goal.enter_one (fun gl -> - Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args)) + let princt = Retyping.get_type_of (pf_env gl) sigma princ in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.tclUNIT (princ, Tactypes.NoBindings, princt, args) | _ -> CErrors.user_err (str "functional induction must be used with a function" ) end | Some ((princ,binding)) -> - Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args) + let sigma, princt = pf_type_of gl princ in + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.tclUNIT (princ, binding, princt, args) ) >>= fun (princ, bindings, princ_type, args) -> Proofview.Goal.enter (fun gl -> let sigma = project gl in diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index b55d8537d6..bce09d8fbd 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -526,3 +526,7 @@ let funind_purify f x = let e = CErrors.push e in Vernacstate.unfreeze_interp_state st; Exninfo.iraise e + +let tac_type_of g c = + let sigma, t = Tacmach.pf_type_of g c in + {g with Evd.sigma}, t diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 550f727951..bd8b34088b 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -119,3 +119,5 @@ type tcc_lemma_value = | Not_needed val funind_purify : ('a -> 'b) -> ('a -> 'b) + +val tac_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Goal.goal Evd.sigma * EConstr.types diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d72319d078..332d058ce7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -28,7 +28,7 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> let sigma = project gl in - let typ = pf_unsafe_type_of gl (mkVar hid) in + let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App(i,args) when isInd sigma i -> let ((kn',num) as ind'),u = destInd sigma i in @@ -77,7 +77,7 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in let sigma = project gl in - let type_of_h = pf_unsafe_type_of gl (mkVar hid) in + let type_of_h = pf_get_hyp_typ hid gl in match EConstr.kind sigma type_of_h with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> let pre_tac,f_args,res = @@ -128,7 +128,7 @@ let invfun qhyp f = | None -> let tac_action hid gl = let sigma = project gl in - let hyp_typ = pf_unsafe_type_of gl (mkVar hid) in + let hyp_typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma hyp_typ with | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) -> begin diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 66ed1961ba..f7f8004998 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -31,7 +31,6 @@ open Tactics open Nametab open Declare open Tacred -open Goal open Glob_term open Pretyping open Termops @@ -110,9 +109,10 @@ let pf_get_new_ids idl g = 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 = +let compute_renamed_type gls id = rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] - (pf_unsafe_type_of gls c) + (pf_get_hyp_typ gls id) + let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" let ano_id = Id.of_string "anonymous" @@ -370,7 +370,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic = Proofview.V82.of_tactic (clear to_intros); h_intros to_intros; (fun g' -> - let ty_teq = pf_unsafe_type_of g' (mkVar heq) in + let ty_teq = pf_get_hyp_typ g' heq in let teq_lhs,teq_rhs = let _,args = try destApp (project g') ty_teq with DestKO -> assert false in args.(1),args.(2) @@ -487,13 +487,13 @@ let rec prove_lt hyple g = in let h = List.find (fun id -> - match decompose_app sigma (pf_unsafe_type_of g (mkVar id)) with + match decompose_app sigma (pf_get_hyp_typ g id) with | _, t::_ -> EConstr.eq_constr sigma t varx | _ -> false ) hyple in let y = - List.hd (List.tl (snd (decompose_app sigma (pf_unsafe_type_of g (mkVar h))))) in + List.hd (List.tl (snd (decompose_app sigma (pf_get_hyp_typ g h)))) in observe_tclTHENLIST (fun _ _ -> str "prove_lt1")[ Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))); observe_tac (fun _ _ -> str "prove_lt") (prove_lt hyple) @@ -645,9 +645,7 @@ let pf_typel l tac = modified hypotheses are generalized in the process and should be 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 Evd.sigma -> tactic * Id.t list = - fun not_on_hyp expr g -> +let mkDestructEq not_on_hyp expr g = let hyps = pf_hyps g in let to_revert = Util.List.map_filter @@ -657,9 +655,9 @@ let mkDestructEq : 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 - let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|]):: - to_revert_constr in + let g, type_of_expr = tac_type_of g expr in + let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::to_revert_constr in + let tac = pf_typel new_hyps (fun _ -> observe_tclTHENLIST (fun _ _ -> str "mkDestructEq") [Proofview.V82.of_tactic (generalize new_hyps); @@ -668,7 +666,9 @@ let mkDestructEq : pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in Proofview.V82.of_tactic (change_in_concl ~check:true None changefun) g2); - Proofview.V82.of_tactic (simplest_case expr)]), to_revert + Proofview.V82.of_tactic (simplest_case expr)]) + in + g, tac, to_revert let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = let sigma = project g in @@ -686,7 +686,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g = info = mkCase(ci,t,a',l); is_main_branch = expr_info.is_main_branch; is_final = expr_info.is_final} in - let destruct_tac,rev_to_thin_intro = + let g,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 (fun _ _ -> str "treating cases (" ++ int (Array.length l) ++ str")" ++ spc () ++ Printer.pr_leconstr_env (pf_env g) sigma a') @@ -842,7 +842,7 @@ let rec make_rewrite_list expr_info max = function (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 t_eq = compute_renamed_type g hp in let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in @@ -868,7 +868,7 @@ let make_rewrite expr_info l hp max = (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 t_eq = compute_renamed_type g hp in let k,def = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in |