From 2bc88f9a536c3db3c2d4a38a8a0da0500b895c7b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 14 Sep 2015 18:35:48 +0200 Subject: Univs: Add universe binding lists to definitions ... lemmas and inductives to control which universes are bound and where in universe polymorphic definitions. Names stay outside the kernel. --- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 26 +++++++++++++------------- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 8 ++------ 4 files changed, 17 insertions(+), 21 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 065c12a2d7..07efaae27b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1395,7 +1395,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - ((Loc.ghost,relnames.(i)), + (((Loc.ghost,relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5dcb0c0439..d9d059f8fa 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -150,7 +150,7 @@ let build_newrecursive in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) ((_,recname),bl,arityc,_) -> + (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.prod_constr_expr arityc bl in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evdref = ref (Evd.from_env env0) in @@ -323,7 +323,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function ((_, name),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in @@ -343,7 +343,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error locate_ind f_R_mut) in - let fname_kn ((fname,_,_,_,_),_) = + let fname_kn (((fname,_),_,_,_,_),_) = let f_ref = Ident fname in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") @@ -380,15 +380,15 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with - | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> + | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in Command.do_definition fname - (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) + (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left - (fun (evd,l) (((_,fname),_,_,_,_),_) -> + (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -402,7 +402,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) (((_,fname),_,_,_,_),_) -> + (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -614,7 +614,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let _is_struct = match fixpoint_exprl with | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> - let ((((_,name),_,args,types,body)),_) as fixpoint_expr = + let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; false |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> - let ((((_,name),_,args,types,body)),_) as fixpoint_expr = + let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -672,7 +672,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in let fix_names = - List.map (function (((_,name),_,_,_,_),_) -> name) fixpoint_exprl + List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in @@ -867,20 +867,20 @@ let make_graph (f_ref:global_reference) = ) in let b' = add_args (snd id) new_args b in - (((id, ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + ((((id,None), ( Some (Loc.ghost,rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (con_label c) in - [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [(((Loc.ghost,id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = repr_con c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) + (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) expr_list); Dumpglob.continue () diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ea699580b9..69e055c23b 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -841,7 +841,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = FIXME: params et cstr_expr (arity) *) let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift (rawlist:(Id.t * glob_constr) list) = - let lident = Loc.ghost, shift.ident in + let lident = (Loc.ghost, shift.ident), None in let bindlist , cstr_expr = (* params , arities *) merge_rec_params_and_arity prms1 prms2 shift mkSet in let lcstor_expr : (bool * (lident * constr_expr)) list = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d3979748e1..9de15e4071 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1398,9 +1398,7 @@ let com_terminate start_proof ctx tclIDTAC tclIDTAC; try let sigma, new_goal_type = build_new_goal_type () in - let sigma = - Evd.from_env ~ctx:(Evd.evar_universe_context sigma) Environ.empty_env - in + let sigma = Evd.from_ctx (Evd.evar_universe_context sigma) in open_new_goal start_proof sigma using_lemmas tcc_lemma_ref (Some tcc_lemma_name) @@ -1437,9 +1435,7 @@ let (com_eqn : int -> Id.t -> | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant") in let (evmap, env) = Lemmas.get_current_context() in - let evmap = - Evd.from_env ~ctx:(Evd.evar_universe_context evmap) Environ.empty_env - in + let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) 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) -- cgit v1.2.3 From 836b9faa8797a2802c189e782469f8d2e467d894 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 16:15:05 +0200 Subject: Univs: fix evar_map leaks bugs in Function The evar_map's that are used to typecheck terms must now always be initialized with the global universe graphs using Evd.from_env, so any failure to initialize and thread evar_map's correctly results in errors. --- plugins/funind/functional_principles_types.ml | 20 +++--- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 95 +++++++++++++++------------ plugins/funind/indfun.ml | 34 +++++----- plugins/funind/indfun_common.ml | 7 +- plugins/funind/invfun.ml | 6 +- plugins/funind/recdef.ml | 7 +- 7 files changed, 94 insertions(+), 77 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 3edc590ccc..64284c6fe7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -303,7 +303,8 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let type_sort = Universes.new_sort_in_family InType in + let env = Global.env () in + let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -317,14 +318,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in - let evd' = !evd in let hook = fun new_principle_type _ _ -> if Option.is_empty sorts then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - let s = Universes.new_sort_in_family fam_sort in + let evd' = Evd.from_env (Global.env ()) in + let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in 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' value) in @@ -394,7 +395,7 @@ let get_funs_constant mp dp = let body = Tacred.cbv_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) (Global.env ()) - (Evd.empty) + (Evd.from_env (Global.env ())) body in body @@ -483,11 +484,10 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x) ) fas in - evd:=sigma; (* We create the first priciple by tactic *) let first_type,other_princ_types = match l_schemes with @@ -597,7 +597,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let build_scheme fas = Dumpglob.pause (); - let evd = (ref Evd.empty) in + let evd = (ref (Evd.from_env (Global.env ()))) in let pconstants = (List.map (fun (_,f,sort) -> let f_as_constant = @@ -633,7 +633,7 @@ let build_scheme fas = let build_case_scheme fa = let env = Global.env () - and sigma = Evd.empty in + and sigma = (Evd.from_env (Global.env ())) in (* let id_to_constr id = *) (* Constrintern.global_reference id *) (* in *) @@ -673,14 +673,14 @@ let build_case_scheme fa = ); *) generate_functional_principle - (ref Evd.empty) + (ref (Evd.from_env (Global.env ()))) false scheme_type (Some ([|sorts|])) (Some princ_name) this_block_funs 0 - (prove_princ_for_struct (ref Evd.empty) false 0 [|fst (destConst funs)|]) + (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|]) in () diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61f03d6f22..bc7e6f8b09 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -388,7 +388,7 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) | Some id -> let idref = const_of_id id in (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *) - let idconstr = snd (Evd.fresh_global (Global.env ()) Evd.empty idref) in + let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in (fun u -> constr_head_match u idconstr) (* select only id *) | None -> (fun u -> isApp u) in (* select calls to any function *) let info_list = find_fapp test g in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 07efaae27b..9d3c0b4b46 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -333,20 +333,20 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Option.map (fun x-> fst (Pretyping.understand env Evd.empty x)) raw_value in - let typ,ctx = Pretyping.understand env Evd.empty ~expected_type:Pretyping.IsType raw_typ in + let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in + let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in Environ.push_named (id,value,typ) env let add_pat_variables 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.empty); + observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with | PatVar(_,na) -> Environ.push_rel (na,None,typ) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ + try Inductiveops.find_rectype env (Evd.from_env env) typ with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env = ~init:(env,[]) ) in - observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty); + observe (str "new var env := " ++ Printer.pr_named_context_of res (Evd.from_env env)); res @@ -393,7 +393,7 @@ let rec pattern_to_term_and_type env typ = function constr in let Inductiveops.IndType(indf,indargs) = - try Inductiveops.find_rectype env Evd.empty typ + try Inductiveops.find_rectype env (Evd.from_env env) typ with Not_found -> assert false in let constructors = Inductiveops.get_constructors env indf in @@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ = function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env Evd.empty csta.(i)) + (fun i -> Detyping.detype false [] env (Evd.from_env env) csta.(i)) ) in let patl_as_term = @@ -486,9 +486,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = a pseudo value "v1 ... vn". The "value" of this branch is then simply [res] *) - let rt_as_constr,ctx = Pretyping.understand env Evd.empty rt in - let rt_typ = Typing.unsafe_type_of env Evd.empty rt_as_constr in - let res_raw_type = Detyping.detype false [] env Evd.empty rt_typ in + 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 res_raw_type = Detyping.detype false [] 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 let res_rt = mkGVar res in @@ -594,8 +594,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = and combine the two result *) let v_res = build_entry_lc env funnames avoid v in - let v_as_constr,ctx = Pretyping.understand env Evd.empty v in - let v_type = Typing.unsafe_type_of env Evd.empty v_as_constr 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 new_env = match n with Anonymous -> env @@ -610,10 +610,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let make_discr = make_discr_match brl in build_entry_lc_from_case env funnames make_discr el brl avoid | GIf(_,b,(na,e_option),lhs,rhs) -> - let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr 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 (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -642,10 +642,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = ) nal in - let b_as_constr,ctx = Pretyping.understand env Evd.empty b in - let b_typ = Typing.unsafe_type_of env Evd.empty b_as_constr 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 (ind,_) = - try Inductiveops.find_inductive env Evd.empty b_typ + try Inductiveops.find_inductive env (Evd.from_env env) b_typ with Not_found -> errorlabstrm "" (str "Cannot find the inductive associated to " ++ Printer.pr_glob_constr b ++ str " in " ++ @@ -689,8 +689,8 @@ and build_entry_lc_from_case env funname make_discr in let types = List.map (fun (case_arg,_) -> - let case_arg_as_constr,ctx = Pretyping.understand env Evd.empty case_arg in - Typing.unsafe_type_of env Evd.empty case_arg_as_constr + let case_arg_as_constr,ctx = Pretyping.understand env (Evd.from_env env) case_arg in + Typing.unsafe_type_of env (Evd.from_env env) case_arg_as_constr ) el in (****** The next works only if the match is not dependent ****) @@ -737,11 +737,11 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.fold_right (fun id acc -> let typ_of_id = - Typing.unsafe_type_of env_with_pat_ids Evd.empty (mkVar id) + Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (mkVar id) in let raw_typ_of_id = Detyping.detype false [] - env_with_pat_ids Evd.empty typ_of_id + env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) pat_ids @@ -785,15 +785,15 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve List.map3 (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in - let typ = Detyping.detype false [] new_env Evd.empty typ_as_constr in + let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in List.fold_right (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.empty (mkVar id) in + let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env Evd.empty typ_of_id + Detyping.detype false [] new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -894,7 +894,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let new_t = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in - let t',ctx = Pretyping.understand env Evd.empty new_t in + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -914,7 +914,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = try observe (str "computing new type for eq : " ++ pr_glob_constr rt); let t' = - try fst (Pretyping.understand env Evd.empty t)(*FIXME*) + try fst (Pretyping.understand env (Evd.from_env env) t)(*FIXME*) with e when Errors.noncritical e -> raise Continue in let is_in_b = is_free_in id b in @@ -937,7 +937,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude with Continue -> let jmeq = Globnames.IndRef (fst (destInd (jmeq ()))) in - let ty',ctx = Pretyping.understand env Evd.empty ty in + let ty',ctx = Pretyping.understand env (Evd.from_env env) ty in let ind,args' = Inductive.find_inductive env ty' in let mib,_ = Global.lookup_inductive (fst ind) in let nparam = mib.Declarations.mind_nparams in @@ -949,7 +949,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GRef (Loc.ghost,Globnames.IndRef (fst ind),None), (List.map (fun p -> Detyping.detype false [] - env Evd.empty + env (Evd.from_env env) p) params)@(Array.to_list (Array.make (List.length args' - nparam) @@ -959,7 +959,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = GApp(loc1,GRef(loc2,jmeq,None),[ty;GVar(loc3,id);rt_typ;rt]) in observe (str "computing new type for jmeq : " ++ pr_glob_constr eq'); - let eq'_as_constr,ctx = Pretyping.understand env Evd.empty eq' in + let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in observe (str " computing new type for jmeq : done") ; let new_args = match kind_of_term eq'_as_constr with @@ -978,12 +978,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | Name id' -> (id',Detyping.detype false [] env - Evd.empty + (Evd.from_env env) arg)::acc else if isVar var_as_constr then (destVar var_as_constr,Detyping.detype false [] env - Evd.empty + (Evd.from_env env) arg)::acc else acc ) @@ -1009,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = if is_in_b then b else replace_var_by_term id rt b in let new_env = - let t',ctx = Pretyping.understand env Evd.empty eq' in + let t',ctx = Pretyping.understand env (Evd.from_env env) eq' in Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = @@ -1047,7 +1047,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = else raise Continue with Continue -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1063,7 +1063,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = end | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in let new_env = Environ.push_rel (n,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1082,7 +1082,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in observe (str "computing new type for lambda : " ++ pr_glob_constr rt); - let t',ctx = Pretyping.understand env Evd.empty t in + let t',ctx = Pretyping.understand env (Evd.from_env env) t in match n with | Name id -> let new_env = Environ.push_rel (n,None,t') env in @@ -1104,8 +1104,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | GLetIn(_,n,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in - let t',ctx = Pretyping.understand env Evd.empty t in - let type_t' = Typing.unsafe_type_of env Evd.empty t' in + let evd = (Evd.from_env env) in + let t',ctx = Pretyping.understand env evd t in + let evd = Evd.from_env ~ctx env in + let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1129,7 +1131,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = args (crossed_types) depth t in - let t',ctx = Pretyping.understand env Evd.empty new_t in + let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (na,None,t') env in let new_b,id_to_exclude = rebuild_cons new_env @@ -1297,7 +1299,7 @@ let do_build_inductive let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> Environ.push_named (rel_name,None, - fst (with_full_print (Constrintern.interp_constr env Evd.empty) rel_ar)) env) env relnames rel_arities + fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = @@ -1460,8 +1462,17 @@ let do_build_inductive let build_inductive evd funconstants funsargs returned_types rtl = + let pu = !Detyping.print_universes in + let cu = !Constrextern.print_universes in try - do_build_inductive evd funconstants funsargs returned_types rtl - with e when Errors.noncritical e -> raise (Building_graph e) + Detyping.print_universes := true; + Constrextern.print_universes := true; + do_build_inductive evd funconstants funsargs returned_types rtl; + Detyping.print_universes := pu; + Constrextern.print_universes := cu + with e when Errors.noncritical e -> + Detyping.print_universes := pu; + Constrextern.print_universes := cu; + raise (Building_graph e) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d9d059f8fa..65dc51a84f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -145,15 +145,14 @@ let interp_casted_constr_with_implicits env sigma impls c = let build_newrecursive lnameargsardef = - let env0 = Global.env() - and sigma = Evd.empty - in + let env0 = Global.env() in + let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.prod_constr_expr arityc bl in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in + let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) @@ -228,7 +227,7 @@ let process_vernac_interp_error e = let derive_inversion fix_names = try - let evd' = Evd.empty in + let evd' = Evd.from_env (Global.env ()) in (* we first transform the fix_names identifier into their corresponding constant *) let evd',fix_names_as_constant = List.fold_right @@ -355,9 +354,11 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error List.map_i (fun i x -> let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in - let evd',uprinc = Evd.fresh_global (Global.env ()) !evd princ in + let env = Global.env () in + let evd = ref (Evd.from_env env) in + let evd',uprinc = Evd.fresh_global env !evd princ in let _ = evd := evd' in - let princ_type = Typing.e_type_of ~refresh:true (Global.env ()) evd uprinc in + let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in Functional_principles_types.generate_functional_principle evd interactive_proof @@ -394,7 +395,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in evd,((destConst c)::l) ) - (Evd.empty,[]) + (Evd.from_env (Global.env ()),[]) fixpoint_exprl in evd,List.rev rev_pconstants @@ -408,7 +409,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in evd,((destConst c)::l) ) - (Evd.empty,[]) + (Evd.from_env (Global.env ()),[]) fixpoint_exprl in evd,List.rev rev_pconstants @@ -594,9 +595,9 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in + let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) 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 -> @@ -625,7 +626,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let using_lemmas = [] in let pre_hook pconstants = generate_principle - (ref (Evd.empty)) + (ref (Evd.from_env (Global.env ()))) pconstants on_error true @@ -649,7 +650,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let body = match body with | Some body -> body | None -> user_err_loc (Loc.ghost,"Function",str "Body of Function must be given") in let pre_hook pconstants = generate_principle - (ref Evd.empty) + (ref (Evd.from_env (Global.env ()))) pconstants on_error true @@ -680,7 +681,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let evd,pconstants = if register_built then register_struct is_rec fixpoint_exprl - else (Evd.empty,pconstants) + else (Evd.from_env (Global.env ()),pconstants) in let evd = ref evd in generate_principle @@ -835,10 +836,11 @@ let make_graph (f_ref:global_reference) = | None -> error "Cannot build a graph over an axiom !" | Some body -> let env = Global.env () in + let sigma = Evd.from_env env in let extern_body,extern_type = with_full_print (fun () -> - (Constrextern.extern_constr false env Evd.empty body, - Constrextern.extern_type false env Evd.empty + (Constrextern.extern_constr false env sigma body, + Constrextern.extern_type false env sigma ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type) ) ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 1c409500ef..35bd1c36da 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -180,9 +180,10 @@ let get_proof_clean do_reduce = let with_full_print f a = let old_implicit_args = Impargs.is_implicit_args () and old_strict_implicit_args = Impargs.is_strict_implicit_args () - and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () - in + and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in + let old_printuniverses = !Constrextern.print_universes in + Constrextern.print_universes := true; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -195,6 +196,7 @@ let with_full_print f a = Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); res with @@ -203,6 +205,7 @@ let with_full_print f a = Impargs.make_strict_implicit_args old_strict_implicit_args; Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; + Constrextern.print_universes := old_printuniverses; Dumpglob.continue (); raise reraise diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 89ceb751a4..d979401424 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -760,7 +760,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs_constr = Array.map mkConstU funs in States.with_state_protection_on_exception (fun () -> - let evd = ref Evd.empty in + let env = Global.env () in + let evd = ref (Evd.from_env env) in let graphs_constr = Array.map mkInd graphs in let lemmas_types_infos = Util.Array.map2_i @@ -829,7 +830,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( ) funs; - (* let evd = ref Evd.empty in *) let lemmas_types_infos = Util.Array.map2_i (fun i f_constr graph -> @@ -875,7 +875,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( 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)) !evd + (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 diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 9de15e4071..ca0b9c5feb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -194,7 +194,7 @@ let (value_f:constr list -> global_reference -> constr) = Anonymous)], GVar(d0,v_id)]) in - let body = fst (understand env Evd.empty glob_body)(*FIXME*) in + let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) = @@ -1293,8 +1293,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp ref_ := Some lemma ; let lid = ref [] in let h_num = ref (-1) in + let env = Global.env () in Proof_global.discard_all (); - build_proof Evd.empty + build_proof (Evd.from_env env) ( fun gls -> let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") @@ -1513,7 +1514,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let relation = fst (*FIXME*)(interp_constr env_with_pre_rec_args - Evd.empty + (Evd.from_env env_with_pre_rec_args) r) in let tcc_lemma_name = add_suffix function_name "_tcc" in -- cgit v1.2.3 From c92946243ccb0b11cd138f040a5297979229c3f5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 23 Sep 2015 19:01:31 +0200 Subject: Univs: fix after rebase (from_ctx/from_env) --- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/indfun.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 9d3c0b4b46..1b12cd42ce 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1106,7 +1106,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in - let evd = Evd.from_env ~ctx env in + let evd = Evd.from_ctx ctx in let type_t' = Typing.unsafe_type_of env evd t' in let new_env = Environ.push_rel (n,Some t',type_t') env in let new_b,id_to_exclude = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 65dc51a84f..eadeebd38e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -597,7 +597,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = - with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_env ~ctx (Global.env ())))) typel in + with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) 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 -> -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_termops.mli | 4 ++-- plugins/funind/merge.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index bc7e6f8b09..e7732a5037 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -379,7 +379,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list = (** [finduction id filter g] tries to apply functional induction on - an occurence of function [id] in the conclusion of goal [g]. If + an occurrence of function [id] in the conclusion of goal [g]. If [id]=[None] then calls to any function are selected. In any case [heuristic] is used to select the most pertinent occurrence. *) let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 0f10636f0f..179e8fe8d9 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -6,7 +6,7 @@ open Misctypes val get_pattern_id : cases_pattern -> Id.t list (* [pattern_to_term pat] returns a glob_constr corresponding to [pat]. - [pat] must not contain occurences of anonymous pattern + [pat] must not contain occurrences of anonymous pattern *) val pattern_to_term : cases_pattern -> glob_constr @@ -64,7 +64,7 @@ val change_vars : Id.t Id.Map.t -> glob_constr -> glob_constr (* [alpha_pat avoid pat] rename all the variables present in [pat] s.t. the result does not share variables with [avoid]. This function create - a fresh variable for each occurence of the anonymous pattern. + a fresh variable for each occurrence of the anonymous pattern. Also returns a mapping from old variables to new ones and the concatenation of [avoid] with the variables appearing in the result. diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 69e055c23b..60c58730a3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -902,7 +902,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs - [ind1] and [ind2]. identifiers occuring in both arrays [args1] and + [ind1] and [ind2]. identifiers occurring in both arrays [args1] and [args2] are considered linked (i.e. are the same variable) in the new graph. -- cgit v1.2.3 From 70d3ad33f6ba7a1c6b1fb93aadd5c05d7e9c03b8 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 11:49:38 +0200 Subject: Partly fixes #3225. Removed some old experimental stuff in funind. --- plugins/funind/g_indfun.ml4 | 244 -------------------------------------------- 1 file changed, 244 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index e7732a5037..045beb37cf 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -247,247 +247,3 @@ END VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY ["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ] END - - - - - -(* FINDUCTION *) - -(* comment this line to see debug msgs *) -let msg x = () ;; let pr_lconstr c = str "" - (* uncomment this to see debugging *) -let prconstr c = msg (str" " ++ Printer.pr_lconstr c ++ str"\n") -let prlistconstr lc = List.iter prconstr lc -let prstr s = msg(str s) -let prNamedConstr s c = - begin - msg(str ""); - msg(str(s^"==>\n ") ++ Printer.pr_lconstr c ++ str "\n<==\n"); - msg(str ""); - end - - - -(** Information about an occurrence of a function call (application) - inside a term. *) -type fapp_info = { - fname: constr; (** The function applied *) - largs: constr list; (** List of arguments *) - free: bool; (** [true] if all arguments are debruijn free *) - max_rel: int; (** max debruijn index in the funcall *) - onlyvars: bool (** [true] if all arguments are variables (and not debruijn) *) -} - - -(** [constr_head_match(a b c) a] returns true, false otherwise. *) -let constr_head_match u t= - if isApp u - then - let uhd,args= destApp u in - Constr.equal uhd t - else false - -(** [hdMatchSub inu t] returns the list of occurrences of [t] in - [inu]. DeBruijn are not pushed, so some of them may be unbound in - the result. *) -let rec hdMatchSub inu (test: constr -> bool) : fapp_info list = - let subres = - match kind_of_term inu with - | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> - hdMatchSub tp test @ hdMatchSub (lift 1 cstr) test - | Fix (_,(lna,tl,bl)) -> (* not sure Fix is correct *) - Array.fold_left - (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) test) - [] bl - | _ -> (* Cofix will be wrong *) - fold_constr - (fun l cstr -> - l @ hdMatchSub cstr test) [] inu in - if not (test inu) then subres - else - let f,args = decompose_app inu in - let freeset = Termops.free_rels inu in - let max_rel = try Int.Set.max_elt freeset with Not_found -> -1 in - {fname = f; largs = args; free = Int.Set.is_empty freeset; - max_rel = max_rel; onlyvars = List.for_all isVar args } - ::subres - -let make_eq () = -(*FIXME*) Universes.constr_of_global (Coqlib.build_coq_eq ()) - -let mkEq typ c1 c2 = - mkApp (make_eq(),[| typ; c1; c2|]) - - -let poseq_unsafe idunsafe cstr gl = - let typ = Tacmach.pf_unsafe_type_of gl cstr in - tclTHEN - (Proofview.V82.of_tactic (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)) - (tclTHENFIRST - (Proofview.V82.of_tactic (Tactics.assert_before Anonymous (mkEq typ (mkVar idunsafe) cstr))) - (Proofview.V82.of_tactic Tactics.reflexivity)) - gl - - -let poseq id cstr gl = - let x = Tactics.fresh_id [] id gl in - poseq_unsafe x cstr gl - -(* dirty? *) - -let list_constr_largs = ref [] - -let rec poseq_list_ids_rec lcstr gl = - match lcstr with - | [] -> tclIDTAC gl - | c::lcstr' -> - match kind_of_term c with - | Var _ -> - (list_constr_largs:=c::!list_constr_largs ; poseq_list_ids_rec lcstr' gl) - | _ -> - let _ = prstr "c = " in - let _ = prconstr c in - let _ = prstr "\n" in - let typ = Tacmach.pf_unsafe_type_of gl c in - let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in - let x = Tactics.fresh_id [] cname gl in - let _ = list_constr_largs:=mkVar x :: !list_constr_largs in - let _ = prstr " list_constr_largs = " in - let _ = prlistconstr !list_constr_largs in - let _ = prstr "\n" in - - tclTHEN - (poseq_unsafe x c) - (poseq_list_ids_rec lcstr') - gl - -let poseq_list_ids lcstr gl = - let _ = list_constr_largs := [] in - poseq_list_ids_rec lcstr gl - -(** [find_fapp test g] returns the list of [app_info] of all calls to - functions that satisfy [test] in the conclusion of goal g. Trivial - repetition (not modulo conversion) are deleted. *) -let find_fapp (test:constr -> bool) g : fapp_info list = - let pre_res = hdMatchSub (Tacmach.pf_concl g) test in - let res = - List.fold_right (List.add_set Pervasives.(=)) pre_res [] in - (prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) res); - res) - - - -(** [finduction id filter g] tries to apply functional induction on - an occurrence of function [id] in the conclusion of goal [g]. If - [id]=[None] then calls to any function are selected. In any case - [heuristic] is used to select the most pertinent occurrence. *) -let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list) - (nexttac:Proof_type.tactic) g = - let test = match oid with - | Some id -> - let idref = const_of_id id in - (* JF : FIXME : we probably need to keep trace of evd in presence of universe polymorphism *) - let idconstr = snd (Evd.fresh_global (Global.env ()) (Evd.from_env (Global.env ())) idref) in - (fun u -> constr_head_match u idconstr) (* select only id *) - | None -> (fun u -> isApp u) in (* select calls to any function *) - let info_list = find_fapp test g in - let ordered_info_list = heuristic info_list in - prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list); - if List.is_empty ordered_info_list then Errors.error "function not found in goal\n"; - let taclist: Proof_type.tactic list = - List.map - (fun info -> - (tclTHEN - (tclTHEN (poseq_list_ids info.largs) - ( - fun gl -> - (functional_induction - true (applist (info.fname, List.rev !list_constr_largs)) - None None) gl)) - nexttac)) ordered_info_list in - (* we try each (f t u v) until one does not fail *) - (* TODO: try also to mix functional schemes *) - tclFIRST taclist g - - - - -(** [chose_heuristic oi x] returns the heuristic for reordering - (and/or forgetting some elts of) a list of occurrences of - function calls infos to chose first with functional induction. *) -let chose_heuristic (oi:int option) : fapp_info list -> fapp_info list = - match oi with - | Some i -> (fun l -> [ List.nth l (i-1) ]) (* occurrence was given by the user *) - | None -> - (* Default heuristic: put first occurrences where all arguments - are *bound* (meaning already introduced) variables *) - let ordering x y = - if x.free && x.onlyvars && y.free && y.onlyvars then 0 (* both pertinent *) - else if x.free && x.onlyvars then -1 - else if y.free && y.onlyvars then 1 - else 0 (* both not pertinent *) - in - List.sort ordering - - - -TACTIC EXTEND finduction - ["finduction" ident(id) natural_opt(oi)] -> - [ - match oi with - | Some(n) when n<=0 -> Errors.error "numerical argument must be > 0" - | _ -> - let heuristic = chose_heuristic oi in - Proofview.V82.tactic (finduction (Some id) heuristic tclIDTAC) - ] -END - - - -TACTIC EXTEND fauto - [ "fauto" tactic(tac)] -> - [ - let heuristic = chose_heuristic None in - Proofview.V82.tactic (finduction None heuristic (Proofview.V82.of_tactic (Tacinterp.eval_tactic tac))) - ] - | - [ "fauto" ] -> - [ - let heuristic = chose_heuristic None in - Proofview.V82.tactic (finduction None heuristic tclIDTAC) - ] - -END - - -TACTIC EXTEND poseq - [ "poseq" ident(x) constr(c) ] -> - [ Proofview.V82.tactic (poseq x c) ] -END - -VERNAC COMMAND EXTEND Showindinfo CLASSIFIED AS QUERY - [ "showindinfo" ident(x) ] -> [ Merge.showind x ] -END - -VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF - [ "Mergeschemes" "(" ident(id1) ne_ident_list(cl1) ")" - "with" "(" ident(id2) ne_ident_list(cl2) ")" "using" ident(id) ] -> - [ - let f1,ctx = Constrintern.interp_constr (Global.env()) Evd.empty - (CRef (Libnames.Ident (Loc.ghost,id1),None)) in - let f2,ctx' = Constrintern.interp_constr (Global.env()) Evd.empty - (CRef (Libnames.Ident (Loc.ghost,id2),None)) in - let f1type = Typing.unsafe_type_of (Global.env()) Evd.empty f1 in - let f2type = Typing.unsafe_type_of (Global.env()) Evd.empty f2 in - let ar1 = List.length (fst (decompose_prod f1type)) in - let ar2 = List.length (fst (decompose_prod f2type)) in - let _ = - if not (Int.equal ar1 (List.length cl1)) then - Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in - let _ = - if not (Int.equal ar2 (List.length cl2)) then - Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in - Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2) id - ] -END -- cgit v1.2.3 From 6f6b67d3f772205d9481436d62efb6074e975555 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Mon, 19 Oct 2015 11:17:56 +0200 Subject: Function debug mode more formatted. --- plugins/funind/functional_principles_proofs.ml | 4 ++-- plugins/funind/invfun.ml | 4 ++-- plugins/funind/recdef.ml | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 169a706005..c9dd18a2fc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -52,10 +52,10 @@ let rec print_debug_queue e = let _ = match e with | Some e -> - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 0 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) | None -> begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (str " from " ++ lmsg ++ str " on goal" ++ fnl() ++ goal); end in print_debug_queue None ; end diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d979401424..d074bbabd8 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -70,8 +70,8 @@ let do_observe_tac s tac g = with reraise -> let reraise = Errors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in - observe (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal " ++ goal ); + observe (hov 0 (str "observation "++ s++str " raised exception " ++ + Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ac7140b9b4..aaeb577d39 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -212,10 +212,10 @@ let rec print_debug_queue b e = begin let lmsg,goal = Stack.pop debug_queue in if b then - Pp.msg_debug (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal) + Pp.msg_debug (hov 1 (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal" ++ fnl() ++ goal)) else begin - Pp.msg_debug (str " from " ++ lmsg ++ str " on goal " ++ goal); + Pp.msg_debug (hov 1 (str " from " ++ lmsg ++ str " on goal"++fnl() ++ goal)); end; (* print_debug_queue false e; *) end -- cgit v1.2.3 From 666568377cbe1c18ce479d32f6359aa61af6d553 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 19 Oct 2015 16:36:53 +0200 Subject: Type delayed_open_constr is now monotonic. --- plugins/funind/indfun.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eadeebd38e..ab3629f89e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,6 +10,7 @@ open Glob_term open Declarations open Misctypes open Decl_kinds +open Sigma.Notations let is_rec_info scheme_info = let test_branche min acc (_,_,br) = @@ -86,7 +87,7 @@ let functional_induction with_clean c princl pat = in let encoded_pat_as_patlist = List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None)) + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None)) (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in -- cgit v1.2.3 From 1235c6c3cfc6770920f46de30b1c4b0f5cb44b19 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 28 Oct 2015 12:49:03 +0100 Subject: Do not pause globing in funind. (Fix bug #4382) Since the functions of this plugin exit by raising exceptions, globing was never restarted. This prevented coqdoc from generating a proper output whenever some feature of this plugin was used. There does not seem to be any parsing of dynamic expressions, so pausing globing does not make much sense in the first place. --- plugins/funind/functional_principles_types.ml | 7 +------ plugins/funind/indfun.ml | 9 ++------- 2 files changed, 3 insertions(+), 13 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 64284c6fe7..9e27ddf2e9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -594,9 +594,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr in const::other_result - let build_scheme fas = - Dumpglob.pause (); let evd = (ref (Evd.from_env (Global.env ()))) in let pconstants = (List.map (fun (_,f,sort) -> @@ -626,10 +624,7 @@ let build_scheme fas = Declare.definition_message princ_id ) fas - bodies_types; - Dumpglob.continue () - - + bodies_types let build_case_scheme fa = let env = Global.env () diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index eadeebd38e..47c67ed2aa 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -27,7 +27,6 @@ let choose_dest_or_ind scheme_info = Tactics.induction_destruct (is_rec_info scheme_info) false let functional_induction with_clean c princl pat = - Dumpglob.pause (); let res = let f,args = decompose_app c in fun g -> @@ -123,9 +122,7 @@ let functional_induction with_clean c princl pat = (args_as_induction_constr,princ'))) subst_and_reduce g' - in - Dumpglob.continue (); - res + in res let rec abstract_glob_constr c = function | [] -> c @@ -831,7 +828,6 @@ let make_graph (f_ref:global_reference) = end | _ -> raise (UserError ("", str "Not a function reference") ) in - Dumpglob.pause (); (match Global.body_of_constant_body c_body with | None -> error "Cannot build a graph over an axiom !" | Some body -> @@ -883,8 +879,7 @@ let make_graph (f_ref:global_reference) = (* We register the infos *) List.iter (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) - expr_list); - Dumpglob.continue () + expr_list) let do_generate_principle = do_generate_principle [] warning_error true -- cgit v1.2.3 From b5a0e384b405f64fd0854d5e88b55e8c2a159c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 11:02:09 -0400 Subject: Univs: fix bug #4375, accept universe binders on (co)-fixpoints --- plugins/funind/indfun.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 47c67ed2aa..3dbd438061 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -592,7 +592,7 @@ let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),ctx,_) = Command.interp_fixpoint fixl ntns in + let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in let constr_expr_typel = with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx))) typel in let fixpoint_exprl_with_new_bl = -- cgit v1.2.3 From 908dcd613b12645f3b62bf44c2696b80a0b16940 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2015 16:46:42 +0100 Subject: Avoid type checking private_constants (side_eff) again during Qed (#4357). Side effects are now an opaque data type, called private_constant, you can only obtain from safe_typing. When add_constant is called on a definition_entry that contains private constants, they are either - inlined in the main proof term but not re-checked - declared globally without re-checking them As a safety measure, the opaque data type contains a pointer to the revstruct (an internal field of safe_env that changes every time a new constant is added), and such pointer is compared with the current value store in safe_env when the private_constant is inlined. Only when the comparison is successful the private_constant is not re-checked. Otherwise else it is. In short, we accept into the kernel private constant only when they arrive in the very same order and on top of the very same env they arrived when we fist checked them. Note: private_constants produced by workers never pass the safety measure (the revstruct pointer is an Ephemeron). Sending back the entire revstruct is possible but: 1. we lack a way to quickly compare two revstructs, 2. it can be large. --- plugins/funind/functional_principles_types.ml | 14 +++++++------- plugins/funind/functional_principles_types.mli | 10 +++++++++- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 4 ++-- 4 files changed, 19 insertions(+), 11 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9e27ddf2e9..c439323243 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (Entries.DefinitionEntry ce, + (DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -447,7 +447,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = +let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = - (Future.from_val (Term_typing.mk_pure_proof princ_body)); - Entries.const_entry_type = Some scheme_type + const_entry_body = + (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + const_entry_type = Some scheme_type } ) other_fun_princ_types @@ -620,7 +620,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index f6e5578d2e..bc082f0730 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* sorts array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Entries.definition_entry list + (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36da..aa47e26192 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 10daf6e848..23f1da1ba7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> unit Lemmas.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and @@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind) + (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) -- cgit v1.2.3 From 0132b5b51fc1856356fb74130d3dea7fd378f76c Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 28 Oct 2015 12:36:20 -0400 Subject: Univs: local names handling. Keep user-side information on the names used in instances of universe polymorphic references and use them for printing. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/merge.ml | 4 ++-- plugins/funind/recdef.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c439323243..c47602bda0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -330,7 +330,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' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(Evd.universe_context evd') value in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in ignore( Declare.declare_constant name diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 60c58730a3..e3455e7702 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,10 +884,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,pl,impls = Command.interp_mutual_inductive indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie impls) + ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca0b9c5feb..5d41ec7237 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1509,7 +1509,7 @@ 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:(Evd.universe_context evm) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = fst (*FIXME*)(interp_constr -- cgit v1.2.3 From f02f64a21863ce03f2da4ff04cd003051f96801f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Oct 2015 18:18:43 +0100 Subject: Removing some goal unsafeness in inductive schemes. --- plugins/funind/functional_principles_types.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda0..bbe2f1a3ad 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -12,6 +12,7 @@ open Tactics open Indfun_common open Functional_principles_proofs open Misctypes +open Sigma.Notations exception Toberemoved_with_rel of int*constr exception Toberemoved @@ -648,12 +649,15 @@ let build_case_scheme fa = 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 in - let ind_fun = + let (ind, sf) = let ind = first_fun_kn,funs_indexes in (ind,Univ.Instance.empty)(*FIXME*),prop_sort in - let sigma, scheme = - (fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf) ind_fun in + let sigma = Sigma.Unsafe.of_evar_map sigma in + let Sigma (scheme, sigma, _) = + Indrec.build_case_analysis_scheme_default env sigma ind sf + in + let sigma = Sigma.to_evar_map sigma in let scheme_type = (Typing.unsafe_type_of env sigma ) scheme in let sorts = (fun (_,_,x) -> -- cgit v1.2.3 From bf1eef119ef8f0e6a2ae4b66165d6e22c1ce9236 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 29 Oct 2015 20:04:58 +0100 Subject: Monotonizing Tactics.change_arg. --- plugins/funind/recdef.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 685a5e8bdf..dd5381c760 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -38,6 +38,7 @@ open Auto open Eauto open Indfun_common +open Sigma.Notations @@ -687,9 +688,12 @@ let mkDestructEq : observe_tclTHENLIST (str "mkDestructEq") [Simple.generalize new_hyps; (fun g2 -> - Proofview.V82.of_tactic (change_in_concl None - (fun patvars sigma -> - pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2); + let changefun patvars = { run = fun sigma -> + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in + Sigma.Unsafe.of_pair (c, sigma) + } in + Proofview.V82.of_tactic (change_in_concl None changefun) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert -- cgit v1.2.3 From 0346ee4472711fc30b7cf197c1bad5c32140f831 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 18 Nov 2015 17:10:44 +0100 Subject: Fix a bug preventing the generation of graphs when doing multiple pattern-matching on function calls. --- plugins/funind/glob_term_to_relation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 1b12cd42ce..5d92fca5ea 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -681,7 +681,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 avoid case_arg in + let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in combine_results combine_args arg_res ctxt_argsl ) el -- cgit v1.2.3 From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- plugins/funind/functional_principles_proofs.ml | 1 + plugins/funind/invfun.ml | 1 + plugins/funind/recdef.ml | 1 + 3 files changed, 3 insertions(+) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c9dd18a2fc..5b9f82aa53 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -9,6 +9,7 @@ open Names open Declarations open Pp open Tacmach +open Termops open Proof_type open Tacticals open Tactics diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d074bbabd8..363dd1b3b7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,6 +19,7 @@ open Tactics open Indfun_common open Tacmach open Misctypes +open Termops (* Some pretty printing function for debugging purpose *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index dd5381c760..6867939c26 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -29,6 +29,7 @@ open Proof_type open Pfedit open Glob_term open Pretyping +open Termops open Constrintern open Misctypes open Genredexpr -- cgit v1.2.3 From aa99912e9adc566a179b4972ff85a92b967fb134 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 7 Dec 2014 22:44:43 +0100 Subject: Removing redundant versions of generalize. --- plugins/funind/functional_principles_proofs.ml | 6 +++--- plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 6 +++--- 3 files changed, 11 insertions(+), 11 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5b9f82aa53..f57f12f667 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -706,7 +706,7 @@ let build_proof in tclTHENSEQ [ - Simple.generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); + generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; pattern_option [Locus.AllOccurrencesBut [1],t] None; (fun g -> observe_tac "toto" ( @@ -933,7 +933,7 @@ let generalize_non_dep hyp g = in (* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *) tclTHEN - ((* observe_tac "h_generalize" *) (Simple.generalize (List.map mkVar to_revert) )) + ((* observe_tac "h_generalize" *) (generalize (List.map mkVar to_revert) )) ((* observe_tac "thin" *) (thin to_revert)) g @@ -1563,7 +1563,7 @@ let prove_principle_for_gen Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = - tclTHEN (Tactics.Simple.generalize (List.map mkVar l)) (clear l) + tclTHEN (Tactics.generalize (List.map mkVar l)) (clear l) in let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 363dd1b3b7..628e582e23 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -458,7 +458,7 @@ let generalize_dependent_of x hyp g = tclMAP (function | (id,None,t) when not (Id.equal id hyp) && - (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.Simple.generalize [mkVar id]) (thin [id]) + (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) (pf_hyps g) @@ -699,7 +699,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = }) Locusops.onConcl ; - Simple.generalize (List.map mkVar ids); + generalize (List.map mkVar ids); thin ids ] else @@ -738,7 +738,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = tclTHENSEQ [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" - (Simple.generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); + (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]); Proofview.V82.of_tactic (Simple.intro graph_principle_id); observe_tac "" (tclTHEN_i (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings))))) @@ -921,7 +921,7 @@ let revert_graph kn post_tac hid g = let f_args,res = Array.chop (Array.length args - 1) args in tclTHENSEQ [ - Simple.generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; + generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); post_tac hid @@ -965,7 +965,7 @@ let functional_inversion kn hid fconst f_correct : tactic = in tclTHENSEQ[ pre_tac hid; - Simple.generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; + generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]; thin [hid]; Proofview.V82.of_tactic (Simple.intro hid); Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid)); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6867939c26..60ff10922c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -687,7 +687,7 @@ let mkDestructEq : to_revert_constr in pf_typel new_hyps (fun _ -> observe_tclTHENLIST (str "mkDestructEq") - [Simple.generalize new_hyps; + [generalize new_hyps; (fun g2 -> let changefun patvars = { run = fun sigma -> let sigma = Sigma.to_evar_map sigma in @@ -1115,7 +1115,7 @@ let termination_proof_header is_mes input_type ids args_id relation [observe_tac (str "generalize") (onNLastHypsId (nargs+1) (tclMAP (fun id -> - tclTHEN (Tactics.Simple.generalize [mkVar id]) (clear [id])) + tclTHEN (Tactics.generalize [mkVar id]) (clear [id])) )) ; observe_tac (str "fix") (fix (Some hrec) (nargs+1)); @@ -1305,7 +1305,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in observe_tclTHENLIST (str "") [ - Simple.generalize [lemma]; + generalize [lemma]; Proofview.V82.of_tactic (Simple.intro hid); (fun g -> let ids = pf_ids_of_hyps g in -- cgit v1.2.3 From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Mon, 7 Dec 2015 10:52:14 +0100 Subject: Fix some typos. --- plugins/funind/functional_principles_proofs.mli | 2 +- plugins/funind/recdef.ml | 12 ++++++------ 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 61fce267a3..34ce669672 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -8,7 +8,7 @@ val prove_princ_for_struct : val prove_principle_for_gen : - constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *) + constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) constr option ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5d41ec7237..951bef2beb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -203,7 +203,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob -(* Debuging mechanism *) +(* Debugging mechanism *) let debug_queue = Stack.create () let rec print_debug_queue b e = @@ -291,9 +291,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress = -(* Travelling term. +(* Traveling term. Both definitions of [f_terminate] and [f_equation] use the same generic - travelling mechanism. + traveling mechanism. *) (* [check_not_nested forbidden e] checks that [e] does not contains any variable @@ -327,7 +327,7 @@ let check_not_nested forbidden e = with UserError(_,p) -> errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p) -(* ['a info] contains the local information for travelling *) +(* ['a info] contains the local information for traveling *) type 'a infos = { nb_arg : int; (* function number of arguments *) concl_tac : tactic; (* final tactic to finish proofs *) @@ -337,7 +337,7 @@ type 'a infos = f_id : Id.t; (* function name *) f_constr : constr; (* function term *) f_terminate : constr; (* termination proof term *) - func : global_reference; (* functionnal reference *) + func : global_reference; (* functional reference *) info : 'a; is_main_branch : bool; (* on the main branch or on a matched expression *) is_final : bool; (* final first order term or not *) @@ -357,7 +357,7 @@ type ('a,'b) journey_info_tac = 'b infos -> (* argument of the tactic *) tactic -(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term +(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term *) type journey_info = { letiN : ((Name.t*constr*types*constr),constr) journey_info_tac; -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- plugins/funind/indfun.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index bf9da870e4..7815a8f818 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -728,9 +728,9 @@ let rec add_args id new_args b = List.map (fun (e,o) -> add_args id new_args e,o) bl) | CCases(loc,sty,b_option,cel,cal) -> CCases(loc,sty,Option.map (add_args id new_args) b_option, - List.map (fun (b,(na,b_option)) -> + List.map (fun (b,na,b_option) -> add_args id new_args b, - (na, b_option)) cel, + na, b_option) cel, List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal ) | CLetTuple(loc,nal,(na,b_option),b1,b2) -> -- cgit v1.2.3 From 77e6eda6388aba117476f6c8445c4b61ebdbc33e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 00:44:58 +0100 Subject: Tentative API fix for tactic arguments to be fed to tclWITHHOLES. The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. --- plugins/funind/g_indfun.ml4 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 045beb37cf..cba10ca09d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -55,7 +55,9 @@ let pr_with_bindings_typed prc prlc (c,bl) = let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) + | Some b -> + let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in + spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) ARGUMENT EXTEND fun_ind_using -- cgit v1.2.3 From 28d4740736e5ef3b6f8547710dcf7e5b4d11cabd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 19:57:14 +0100 Subject: Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr. --- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/recdef.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f57f12f667..1474f1e936 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1473,7 +1473,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = tclCOMPLETE( Eauto.eauto_with_bases (true,5) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ) ) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5a30da336e..10a145e036 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1335,7 +1335,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) - [Evd.empty,Lazy.force refl_equal] + [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}] [Hints.Hint_db.empty empty_transparent_state false] ] ) -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- plugins/funind/functional_principles_proofs.ml | 3 +-- plugins/funind/functional_principles_types.ml | 3 +-- plugins/funind/glob_term_to_relation.ml | 2 +- plugins/funind/merge.ml | 19 +++++++++---------- 4 files changed, 12 insertions(+), 15 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index f57f12f667..ad18ea95a4 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -3,7 +3,6 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Declarations @@ -230,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta -let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = +let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = let nochange ?t' msg = begin observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t ++ str " " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t ); diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index bbe2f1a3ad..e2c3bbb978 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -3,7 +3,6 @@ open Errors open Util open Term open Vars -open Context open Namegen open Names open Pp @@ -30,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let env = Global.env () in let env_with_params = Environ.push_rel_context princ_type_info.params env in let tbl = Hashtbl.create 792 in - let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context) : rel_context = + let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = match predicates with | [] -> [] |(Name x,v,t)::predicates -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 5d92fca5ea..80de8e764d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env = let new_env = add_pat_variables env pat typ in let res = fst ( - Context.fold_rel_context + Context.Rel.fold_outside (fun (na,v,t) (env,ctxt) -> match na with | Anonymous -> assert false diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index e3455e7702..be04728e03 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -19,7 +19,6 @@ open Pp open Names open Term open Vars -open Context open Termops open Declarations open Glob_term @@ -258,27 +257,27 @@ type merge_infos = lnk2: int merged_arg array; (** rec params which remain rec param (ie not linked) *) - recprms1: rel_declaration list; - recprms2: rel_declaration list; + recprms1: Context.Rel.Declaration.t list; + recprms2: Context.Rel.Declaration.t list; nrecprms1: int; nrecprms2: int; (** rec parms which became non parm (either linked to something or because after a rec parm that became non parm) *) - otherprms1: rel_declaration list; - otherprms2: rel_declaration list; + otherprms1: Context.Rel.Declaration.t list; + otherprms2: Context.Rel.Declaration.t list; notherprms1:int; notherprms2:int; (** args which remain args in merge *) - args1:rel_declaration list; - args2:rel_declaration list; + args1:Context.Rel.Declaration.t list; + args2:Context.Rel.Declaration.t list; nargs1:int; nargs2:int; (** functional result args *) - funresprms1: rel_declaration list; - funresprms2: rel_declaration list; + funresprms1: Context.Rel.Declaration.t list; + funresprms2: Context.Rel.Declaration.t list; nfunresprms1:int; nfunresprms2:int; } @@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift lident , bindlist , Some cstr_expr , lcstor_expr -let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) = +let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] (Global.env()) Evd.empty t in -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- plugins/funind/indfun.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 7815a8f818..d1e1098259 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -752,10 +752,8 @@ let rec add_args id new_args b = | CCast(loc,b1,b2) -> CCast(loc,add_args id new_args b1, Miscops.map_cast_type (add_args id new_args) b2) - | CRecord (loc, w, pars) -> - CRecord (loc, - (match w with Some w -> Some (add_args id new_args w) | _ -> None), - List.map (fun (e,o) -> e, add_args id new_args o) pars) + | CRecord (loc, pars) -> + CRecord (loc, List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation") | CGeneralization _ -> anomaly ~label:"add_args " (Pp.str "CGeneralization") | CPrim _ -> b -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/funind/Recdef.v | 2 +- plugins/funind/functional_principles_types.mli | 2 +- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 2 +- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 2 +- 6 files changed, 6 insertions(+), 6 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index a63941f0cb..e4433247b4 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- plugins/funind/functional_principles_proofs.ml | 60 ++++++++++++++------------ plugins/funind/functional_principles_types.ml | 39 ++++++++++------- plugins/funind/glob_term_to_relation.ml | 52 ++++++++++++---------- plugins/funind/indfun.ml | 8 ++-- plugins/funind/invfun.ml | 40 +++++++++-------- plugins/funind/merge.ml | 24 ++++++----- plugins/funind/recdef.ml | 18 ++++---- 7 files changed, 136 insertions(+), 105 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4eab5f9126..28982c37fe 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -15,6 +15,7 @@ open Tactics open Indfun_common open Libnames open Globnames +open Context.Rel.Declaration (* let msgnl = Pp.msgnl *) @@ -304,11 +305,11 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = in let new_type_of_hyp,ctxt_size,witness_fun = List.fold_left_i - (fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) -> + (fun i (end_of_type,ctxt_size,witness_fun) decl -> try let witness = Int.Map.find i sub in - if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!"); - (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun)) + if is_local_def decl then anomaly (Pp.str "can not redefine a rel!"); + (Termops.pop end_of_type,ctxt_size,mkLetIn (get_name decl, witness, get_type decl, witness_fun)) with Not_found -> (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun) ) @@ -536,7 +537,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = (scan_type new_context new_t') with Failure "NoChange" -> (* Last thing todo : push the rel in the context and continue *) - scan_type ((x,None,t_x)::context) t' + scan_type (LocalAssum (x,t_x) :: context) t' end end else @@ -736,7 +737,8 @@ let build_proof tclTHEN (Proofview.V82.of_tactic intro) (fun g' -> - let (id,_,_) = pf_last_hyp g' in + let open Context.Named.Declaration in + let id = pf_last_hyp g' |> get_id in let new_term = pf_nf_betaiota g' (mkApp(dyn_infos.info,[|mkVar id|])) @@ -921,7 +923,9 @@ let generalize_non_dep hyp g = let env = Global.env () in let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in let to_revert,_ = - Environ.fold_named_context_reverse (fun (clear,keep) (hyp,_,_ as decl) -> + let open Context.Named.Declaration in + Environ.fold_named_context_reverse (fun (clear,keep) decl -> + let hyp = get_id decl in if Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env hyp) keep || Termops.occur_var env hyp hyp_typ @@ -936,7 +940,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl (na,_,_) = (Nameops.out_name na) +let id_of_decl decl = Nameops.out_name (get_name decl) let var_of_decl decl = mkVar (id_of_decl decl) let revert idl = tclTHEN @@ -1044,7 +1048,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a ( fun g' -> let just_introduced = nLastDecls nb_intro_to_do g' in - let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in + let open Context.Named.Declaration in + let just_introduced_id = List.map get_id just_introduced in tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma)) (revert just_introduced_id) g' ) @@ -1069,11 +1074,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (Name new_id) ) in - let fresh_decl = - (fun (na,b,t) -> - (fresh_id na,b,t) - ) - in + let fresh_decl = map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1120,11 +1121,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (fun (na,_,_) -> Ppconstr.pr_id (Nameops.out_name na)) + prlist_with_sep spc (fun decl -> Ppconstr.pr_id (Nameops.out_name (get_name decl))) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1165,7 +1166,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let pte_to_fix,rev_info = List.fold_left_i - (fun i (acc_map,acc_info) (pte,_,_) -> + (fun i (acc_map,acc_info) decl -> + let pte = get_name decl in let infos = info_array.(i) in let type_args,_ = decompose_prod infos.types in let nargs = List.length type_args in @@ -1259,7 +1261,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) - let args_id = List.map (fun (id,_,_) -> id) args in + let open Context.Named.Declaration in + let args_id = List.map get_id args in let dyn_infos = { nb_rec_hyps = -100; @@ -1276,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (fun (id,_,_) -> Nameops.out_name id ) princ_params)) + (args_id@(List.map (fun decl -> Nameops.out_name (get_name decl)) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1317,8 +1320,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam [ tclDO nb_args (Proofview.V82.of_tactic intro); (fun g -> (* replacement of the function by its body *) - let args = nLastDecls nb_args g in - let args_id = List.map (fun (id,_,_) -> id) args in + let args = nLastDecls nb_args g in + let open Context.Named.Declaration in + let args_id = List.map get_id args in let dyn_infos = { nb_rec_hyps = -100; @@ -1520,7 +1524,7 @@ let prove_principle_for_gen avoid := new_id :: !avoid; Name new_id in - let fresh_decl (na,b,t) = (fresh_id na,b,t) in + let fresh_decl = map_name fresh_id in let princ_info : elim_scheme = { princ_info with params = List.map fresh_decl princ_info.params; @@ -1550,11 +1554,11 @@ let prove_principle_for_gen in let rec_arg_id = match List.rev post_rec_arg with - | (Name id,_,_)::_ -> id + | (LocalAssum (Name id,_) | LocalDef (Name id,_,_)) :: _ -> id | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (fun decl -> mkVar (Nameops.out_name (get_name decl))) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in @@ -1582,7 +1586,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in + let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in let lemma = match !tcc_lemma_ref with | None -> error "No tcc proof !!" @@ -1629,7 +1633,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (fun (na,_,_) -> Nameops.out_name na) + (List.rev_map (fun decl -> Nameops.out_name (get_name decl)) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1667,7 +1671,7 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates + List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.predicates in let pte_info = { proving_tac = @@ -1683,7 +1687,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (fun (na,_,_) -> (Nameops.out_name na)) + (fun decl -> (Nameops.out_name (get_name decl))) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1712,7 +1716,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches) + (List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index e2c3bbb978..7a933c04b2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -8,6 +8,7 @@ open Names open Pp open Entries open Tactics +open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs open Misctypes @@ -32,11 +33,13 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t) : Context.Rel.t = match predicates with | [] -> [] - |(Name x,v,t)::predicates -> - let id = Namegen.next_ident_away x avoid in - Hashtbl.add tbl id x; - (Name id,v,t)::(change_predicates_names (id::avoid) predicates) - | (Anonymous,_,_)::_ -> anomaly (Pp.str "Anonymous property binder ") + | decl :: predicates -> + (match Context.Rel.Declaration.get_name decl with + | Name x -> + let id = Namegen.next_ident_away x avoid in + Hashtbl.add tbl id x; + set_name (Name id) decl :: change_predicates_names (id::avoid) predicates + | Anonymous -> anomaly (Pp.str "Anonymous property binder ")) in let avoid = (Termops.ids_of_context env_with_params ) in let princ_type_info = @@ -46,15 +49,16 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = in (* observe (str "starting princ_type := " ++ pr_lconstr_env env princ_type); *) (* observe (str "princ_infos : " ++ pr_elim_scheme princ_type_info); *) - let change_predicate_sort i (x,_,t) = + let change_predicate_sort i decl = let new_sort = sorts.(i) in - let args,_ = decompose_prod t in + let args,_ = decompose_prod (get_type decl) in let real_args = if princ_type_info.indarg_in_concl then List.tl args else args in - Nameops.out_name x,None,compose_prod real_args (mkSort new_sort) + Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), + compose_prod real_args (mkSort new_sort)) in let new_predicates = List.map_i @@ -69,7 +73,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | _ -> error "Not a valid predicate" ) in - let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in + let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in let is_pte = let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in fun t -> @@ -114,7 +118,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | Rel n -> begin try match Environ.lookup_rel n env with - | _,_,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 @@ -159,7 +163,7 @@ 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_x : Name.t = get_name (Termops.ids_of_context env) x in - let new_env = Environ.push_rel (x,None,t) env 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 (eq_constr (mkRel 1)) binders_to_remove_from_b then (Termops.pop new_b), filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b @@ -188,7 +192,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = 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 (x,Some v,t) env 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 (eq_constr (mkRel 1)) binders_to_remove_from_b then (Termops.pop new_b),filter_map (eq_constr (mkRel 1)) Termops.pop binders_to_remove_from_b @@ -227,7 +231,8 @@ 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 (fun (id,t,b) -> Name(Hashtbl.find tbl id), t,b) + 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)) new_predicates) ) princ_type_info.params @@ -235,10 +240,12 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let change_property_sort evd toSort princ princName = + let open Context.Rel.Declaration in let princ_info = compute_elim_sig princ in - let change_sort_in_predicate (x,v,t) = - (x,None, - let args,ty = decompose_prod t in + let change_sort_in_predicate decl = + LocalAssum + (get_name decl, + let args,ty = decompose_prod (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); compose_prod args (mkSort toSort) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 80de8e764d..8a0a1a064d 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -335,15 +335,17 @@ let raw_push_named (na,raw_value,raw_typ) env = | Name id -> let value = Option.map (fun x-> fst (Pretyping.understand env (Evd.from_env env) x)) raw_value in let typ,ctx = Pretyping.understand env (Evd.from_env env) ~expected_type:Pretyping.IsType raw_typ in - Environ.push_named (id,value,typ) env + let open Context.Named.Declaration in + Environ.push_named (of_tuple (id,value,typ)) env let add_pat_variables pat typ env : Environ.env = let rec add_pat_variables env pat typ : Environ.env = + let open Context.Rel.Declaration in observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env)); match pat with - | PatVar(_,na) -> Environ.push_rel (na,None,typ) env + | PatVar(_,na) -> Environ.push_rel (LocalAssum (na,typ)) env | PatCstr(_,c,patl,na) -> let Inductiveops.IndType(indf,indargs) = try Inductiveops.find_rectype env (Evd.from_env env) typ @@ -351,15 +353,16 @@ let add_pat_variables pat typ env : Environ.env = in let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + let cs_args_types :types list = List.map 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 res = fst ( Context.Rel.fold_outside - (fun (na,v,t) (env,ctxt) -> - match na with + (fun decl (env,ctxt) -> + let _,v,t = Context.Rel.Declaration.to_tuple decl in + match Context.Rel.Declaration.get_name decl with | Anonymous -> assert false | Name id -> let new_t = substl ctxt t in @@ -370,7 +373,8 @@ let add_pat_variables pat typ env : Environ.env = Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) ); - (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) + let open Context.Named.Declaration in + (Environ.push_named (of_tuple (id,new_v,new_t)) env,mkVar id::ctxt) ) (Environ.rel_context new_env) ~init:(env,[]) @@ -398,7 +402,8 @@ let rec pattern_to_term_and_type env typ = function in let constructors = Inductiveops.get_constructors env indf in let constructor = List.find (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in - let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in + let open Context.Rel.Declaration in + let cs_args_types :types list = List.map get_type constructor.Inductiveops.cs_args in let _,cstl = Inductiveops.dest_ind_family indf in let csta = Array.of_list cstl in let implicit_args = @@ -597,9 +602,10 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = 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 new_env = + let open Context.Named.Declaration in match n with Anonymous -> env - | Name id -> Environ.push_named (id,Some v_as_constr,v_type) env + | Name id -> Environ.push_named (of_tuple (id,Some v_as_constr,v_type)) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_letin n) v_res b_res @@ -875,7 +881,7 @@ exception Continue *) let rec rebuild_cons env nb_args relname args crossed_types depth rt = observe (str "rebuilding : " ++ pr_glob_constr rt); - + let open Context.Rel.Declaration in match rt with | GProd(_,n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in @@ -895,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -926,7 +932,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let subst_b = if is_in_b then b else replace_var_by_term id rt b in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env @@ -970,9 +976,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (fun acc var_as_constr arg -> if isRel var_as_constr then - let (na,_,_) = - Environ.lookup_rel (destRel var_as_constr) env - in + let open Context.Rel.Declaration in + let na = get_name (Environ.lookup_rel (destRel var_as_constr) env) in match na with | Anonymous -> acc | Name id' -> @@ -1010,7 +1015,7 @@ 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 - Environ.push_rel (n,None,t') env + Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons @@ -1048,7 +1053,7 @@ 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 rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1064,7 +1069,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> observe (str "computing new type for prod : " ++ pr_glob_constr rt); let t',ctx = Pretyping.understand env (Evd.from_env env) t in - let new_env = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1085,7 +1090,7 @@ 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 = Environ.push_rel (n,None,t') env in + let new_env = Environ.push_rel (LocalAssum (n,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1108,7 +1113,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = 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 new_env = Environ.push_rel (n,Some t',type_t') env in + let new_env = Environ.push_rel (LocalDef (n,t',type_t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1132,7 +1137,7 @@ 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 = Environ.push_rel (na,None,t') env in + let new_env = Environ.push_rel (LocalAssum (na,t')) env in let new_b,id_to_exclude = rebuild_cons new_env nb_args relname @@ -1254,12 +1259,13 @@ let do_build_inductive let relnames = Array.map mk_rel_id funnames in let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in (* Construction of the pseudo constructors *) + let open Context.Named.Declaration in let evd,env = Array.fold_right2 (fun id c (evd,env) -> let evd,t = Typing.type_of env evd (mkConstU c) in evd, - Environ.push_named (id,None,t) + Environ.push_named (LocalAssum (id,t)) (* try *) (* Typing.e_type_of env evd (mkConstU c) *) (* with Not_found -> *) @@ -1298,8 +1304,8 @@ let do_build_inductive *) let rel_arities = Array.mapi rel_arity funsargs in Util.Array.fold_left2 (fun env rel_name rel_ar -> - Environ.push_named (rel_name,None, - fst (with_full_print (Constrintern.interp_constr env evd) rel_ar)) env) env relnames rel_arities + Environ.push_named (LocalAssum (rel_name, + fst (with_full_print (Constrintern.interp_constr env evd) rel_ar))) env) env relnames rel_arities in (* and of the real constructors*) let constr i res = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d1e1098259..86abf9e2ef 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -1,3 +1,4 @@ +open Context.Rel.Declaration open Errors open Util open Names @@ -13,10 +14,10 @@ open Decl_kinds open Sigma.Notations let is_rec_info scheme_info = - let test_branche min acc (_,_,br) = + let test_branche min acc decl = acc || ( let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum (get_type decl))) in let free_rels_in_br = Termops.free_rels new_branche in let max = min + scheme_info.Tactics.npredicates in Int.Set.exists (fun i -> i >= min && i< max) free_rels_in_br @@ -153,7 +154,8 @@ let build_newrecursive let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in - (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls)) + let open Context.Named.Declaration in + (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb819..56bc4328d1 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -5,6 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + open Tacexpr open Declarations open Errors @@ -20,6 +21,7 @@ open Indfun_common open Tacmach open Misctypes open Termops +open Context.Rel.Declaration (* Some pretty printing function for debugging purpose *) @@ -134,18 +136,21 @@ let generate_type evd g_to_f f graph i = let fun_ctxt,res_type = match ctxt with | [] | [_] -> anomaly (Pp.str "Not a valid context") - | (_,_,res_type)::fun_ctxt -> fun_ctxt,res_type + | decl :: fun_ctxt -> fun_ctxt, get_type decl in let rec args_from_decl i accu = function | [] -> accu - | (_, Some _, _) :: l -> + | LocalDef _ :: l -> args_from_decl (succ i) accu l | _ :: l -> let t = mkRel i in args_from_decl (succ i) (t :: accu) l in (*i We need to name the vars [res] and [fv] i*) - let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in + let filter = fun decl -> match get_name decl with + | Name id -> Some id + | Anonymous -> None + in let named_ctxt = List.map_filter filter fun_ctxt in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in @@ -171,12 +176,12 @@ 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 = - (Name res_id,None,lift 1 res_type)::(Name fv_id,Some (mkApp(f,args_as_rels)),res_type)::fun_ctxt + LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, 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 (Anonymous,None,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph - else (Anonymous,None,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph + 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 (* @@ -260,10 +265,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* and built the intro pattern for each of them *) let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) - (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type)))) + (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (get_type decl))))) ) branches in @@ -390,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun ((_,(ctxt,concl))) -> match ctxt with | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") - | hres::res::(x,_,t)::ctxt -> + | hres::res::decl::ctxt -> let res = Termops.it_mkLambda_or_LetIn (Termops.it_mkProd_or_LetIn concl [hres;res]) - ((x,None,t)::ctxt) + (LocalAssum (get_name decl, get_type decl) :: ctxt) in res ) @@ -408,8 +413,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let bindings = let params_bindings,avoid = List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -418,8 +423,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in let lemmas_bindings = List.rev (fst (List.fold_left2 - (fun (bindings,avoid) (x,_,_) p -> - let id = Namegen.next_ident_away (Nameops.out_name x) avoid in + (fun (bindings,avoid) decl p -> + let id = Namegen.next_ident_away (Nameops.out_name (get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -455,9 +460,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes generalize every hypothesis which depends of [x] but [hyp] *) let generalize_dependent_of x hyp g = + let open Context.Named.Declaration in tclMAP (function - | (id,None,t) when not (Id.equal id hyp) && + | LocalAssum (id,t) when not (Id.equal id hyp) && (Termops.occur_var (pf_env g) x t) -> tclTHEN (Tactics.generalize [mkVar id]) (thin [id]) | _ -> tclIDTAC ) @@ -663,10 +669,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let branches = List.rev princ_infos.branches in let intro_pats = List.map - (fun (_,_,br_type) -> + (fun decl -> List.map (fun id -> id) - (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type)) + (generate_fresh_id (Id.of_string "y") ids (nb_prod (get_type decl))) ) branches in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 57782dd71f..c71d9a9ca4 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -24,6 +24,7 @@ open Declarations open Glob_term open Glob_termops open Decl_kinds +open Context.Rel.Declaration (** {1 Utilities} *) @@ -134,9 +135,9 @@ let showind (id:Id.t) = let cstrid = Constrintern.global_reference id in let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in - List.iter (fun (nm, optcstr, tp) -> - print_string (string_of_name nm^":"); - prconstr tp; print_string "\n") + List.iter (fun decl -> + print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":"); + prconstr (get_type decl); print_string "\n") ib1.mind_arity_ctxt; Printf.printf "arity :"; prconstr (Inductiveops.type_of_inductive (Global.env ()) ind1); Array.iteri @@ -459,11 +460,12 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in let _ = prstr "\notherprms1:\n" in let _ = - List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); + prconstr (get_type decl); prstr "\n") otherprms1 in let _ = prstr "\notherprms2:\n" in let _ = - List.iter (fun (x,_,y) -> prstr (string_of_name x^" : ");prconstr y;prstr "\n") + List.iter (fun decl -> prstr (string_of_name (get_name decl) ^ " : "); prconstr (get_type decl); prstr "\n") otherprms2 in { ident=id; @@ -823,9 +825,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = List.fold_left - (fun (acc,env) (nm,_,c) -> + (fun (acc,env) decl -> + let nm = Context.Rel.Declaration.get_name decl in + let c = get_type decl in let typ = Constrextern.extern_constr false env Evd.empty c in - let newenv = Environ.push_rel (nm,None,c) env in + let newenv = Environ.push_rel (LocalAssum (nm,c)) env in CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @@ -852,10 +856,10 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with - | (nme,None,t) -> + | LocalAssum (nme,t) -> let traw = Detyping.detype false [] (Global.env()) Evd.empty t in GProd (Loc.ghost,nme,Explicit,traw,t2) - | (_,Some _,_) -> assert false + | LocalDef _ -> assert false (** [merge_inductive ind1 ind2 lnk] merges two graphs, linking @@ -969,7 +973,7 @@ let funify_branches relinfo nfuns branch = | Rel i -> let reali = i-shift in (reali>=0 && reali false in (* FIXME: *) - (Anonymous,Some mkProp,mkProp) + LocalDef (Anonymous,mkProp,mkProp) let relprinctype_to_funprinctype relprinctype nfuns = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b096783412..09c5aa5673 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -40,7 +40,7 @@ open Eauto open Indfun_common open Sigma.Notations - +open Context.Rel.Declaration (* Ugly things which should not be here *) @@ -181,7 +181,7 @@ let (value_f:constr list -> global_reference -> constr) = ) in let context = List.map - (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al)) + (fun (x, c) -> LocalAssum (Name x, c)) (List.combine rev_x_id_l (List.rev al)) in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = @@ -678,8 +678,10 @@ let mkDestructEq : let hyps = pf_hyps g in let to_revert = Util.List.map_filter - (fun (id, _, t) -> - if Id.List.mem id not_on_hyp || not (Termops.occur_term expr t) + (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)) 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 @@ -1253,7 +1255,7 @@ let clear_goals = then Termops.pop b' else if b' == b then t else mkProd(na,t',b') - | _ -> map_constr clear_goal t + | _ -> Term.map_constr clear_goal t in List.map clear_goal @@ -1489,7 +1491,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num 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 env = push_named (function_name,None,function_type) env 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 @@ -1497,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let function_type = nf function_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) -> (x,None,y)) res_vars) env 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 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'); *) @@ -1515,7 +1517,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 = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in - let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) 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 = fst (*FIXME*)(interp_constr env_with_pre_rec_args -- cgit v1.2.3 From 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 14:26:43 +0100 Subject: Moving conversion functions to the new tactic API. --- plugins/funind/functional_principles_proofs.ml | 4 ++-- plugins/funind/invfun.ml | 10 +++++----- plugins/funind/recdef.ml | 14 +++++++------- 3 files changed, 14 insertions(+), 14 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 4eab5f9126..aa89f89b74 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1334,7 +1334,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in tclTHENSEQ - [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]; + [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); let do_prove = build_proof interactive_proof @@ -1460,7 +1460,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = (fun g -> if is_mes then - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g else tclIDTAC g ); observe_tac "rew_and_finish" diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c9d3bb819..ae2091a227 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -484,15 +484,15 @@ and intros_with_rewrite_aux : tactic = tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) then tclTHENSEQ[ - unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]; - tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )) + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]); + tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g @@ -703,7 +703,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = thin ids ] else - unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))] + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]) in (* The proof of each branche itself *) let ind_number = ref 0 in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b096783412..834d0aceac 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -276,8 +276,8 @@ let tclUSER tac is_mes l g = if is_mes then observe_tclTHENLIST (str "tclUSER2") [ - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference - (delayed_force Indfun_common.ltof_ref))]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference + (delayed_force Indfun_common.ltof_ref))]); tac ] else tac @@ -564,8 +564,8 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = h_intros [k;h';def]; observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference infos.func)]); + (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], + evaluable_of_global_reference infos.func)])); ( observe_tclTHENLIST (str "test")[ list_rewrite true @@ -904,8 +904,8 @@ let make_rewrite expr_info l hp max = (observe_tclTHENLIST (str "make_rewrite")[ simpl_iter Locusops.onConcl; observe_tac (str "unfold functional") - (unfold_in_concl[(Locus.OnlyOccurrences [1], - evaluable_of_global_reference expr_info.func)]); + (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)); @@ -1425,7 +1425,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; - unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]; + Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]); observe_tac (str "simplest_case") (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))))); -- cgit v1.2.3 From 4ea9b3193eaced958bb277c0723fb54d661ff520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 15:17:05 +0100 Subject: More conversion functions in the new tactic API. --- plugins/funind/functional_principles_proofs.ml | 8 ++++---- plugins/funind/indfun.ml | 2 +- plugins/funind/invfun.ml | 16 ++++++++-------- plugins/funind/recdef.ml | 4 ++-- 4 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index aa89f89b74..86302dc6ce 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -371,12 +371,12 @@ let isLetIn t = | _ -> false -let h_reduce_with_zeta = - reduce +let h_reduce_with_zeta cl = + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; - }) + }) cl) @@ -707,7 +707,7 @@ let build_proof [ generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)); thin dyn_infos.rec_hyps; - pattern_option [Locus.AllOccurrencesBut [1],t] None; + Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); (fun g' -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d1e1098259..41fd0bd18e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -113,7 +113,7 @@ let functional_induction with_clean c princl pat = in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl ) - (Tactics.reduce flag Locusops.allHypsAndConcl) + (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl)) g else Tacticals.tclIDTAC g in diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ae2091a227..2b45206bb4 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -363,14 +363,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (* unfolding of all the defined variables introduced by this branch *) (* observe_tac "unfolding" pre_tac; *) (* $zeta$ normalizing of the conclusion *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false ; Genredexpr.rConst = [] } ) - Locusops.onConcl; + Locusops.onConcl); observe_tac ("toto ") tclIDTAC; (* introducing the the result of the graph and the equality hypothesis *) @@ -532,12 +532,12 @@ and intros_with_rewrite_aux : tactic = ] g | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -547,12 +547,12 @@ and intros_with_rewrite_aux : tactic = end | LetIn _ -> tclTHENSEQ[ - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; intros_with_rewrite ] g @@ -692,12 +692,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *) - reduce + Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags with Genredexpr.rDelta = false; }) - Locusops.onConcl + Locusops.onConcl) ; generalize (List.map mkVar ids); thin ids diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 834d0aceac..6c6caa6284 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -562,7 +562,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g = observe_tclTHENLIST (str "destruct_bounds_aux2")[ observe_tac (str "clearing k ") (clear [id]); h_intros [k;h';def]; - observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl); + observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl)); observe_tac (str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference infos.func)])); @@ -902,7 +902,7 @@ let make_rewrite expr_info l hp max = [observe_tac(str "make_rewrite finalize") ( (* tclORELSE( h_reflexivity) *) (observe_tclTHENLIST (str "make_rewrite")[ - simpl_iter Locusops.onConcl; + Proofview.V82.of_tactic (simpl_iter Locusops.onConcl); observe_tac (str "unfold functional") (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1], evaluable_of_global_reference expr_info.func)])); -- cgit v1.2.3 From 5180ab68819f10949cd41a2458bff877b3ec3204 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 16:45:18 +0100 Subject: Using monotonic types for conversion functions. --- plugins/funind/recdef.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 6c6caa6284..555f08fa86 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -690,9 +690,8 @@ let mkDestructEq : [generalize new_hyps; (fun g2 -> let changefun patvars = { run = fun sigma -> - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in - Sigma.Unsafe.of_pair (c, sigma) + let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in + redfun.Reductionops.e_redfun (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 -- cgit v1.2.3 From 33fe6e61ff2f1f8184373ed8fccc403591c4605a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 21 Feb 2016 17:13:26 +0100 Subject: Moving the Tauto tactic to proper Ltac. This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there. --- plugins/funind/invfun.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cdb9c5067f..6a5a5ad533 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -474,6 +474,15 @@ let generalize_dependent_of x hyp g = (* [intros_with_rewrite] do the intros in each branch and treat each new hypothesis (unfolding, substituting, destructing cases \ldots) *) +let tauto = + let dp = List.map Id.of_string ["Tauto" ; "Init"; "Coq"] in + let mp = ModPath.MPfile (DirPath.make dp) in + let kn = KerName.make2 mp (Label.make "tauto") in + Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () -> + let body = Tacenv.interp_ltac kn in + Tacinterp.eval_tactic body + end + let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g and intros_with_rewrite_aux : tactic = @@ -530,7 +539,7 @@ and intros_with_rewrite_aux : tactic = ] g end | Ind _ when eq_constr t (Coqlib.build_coq_False ()) -> - Proofview.V82.of_tactic Tauto.tauto g + Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ Proofview.V82.of_tactic (simplest_case v); -- cgit v1.2.3 From b98e4857a13a4014c65882af5321ebdb09f41890 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 4 Mar 2016 17:40:10 +0100 Subject: Rename Ephemeron -> CEphemeron. Fixes compilation of Coq with OCaml 4.03 beta 1. --- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/indfun_common.ml | 2 +- plugins/funind/indfun_common.mli | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index c47602bda0..18200307a8 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -291,7 +291,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* 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, Ephemeron.create hook + get_proof_clean true, CEphemeron.create hook end diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index aa47e26192..2449678a13 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook = (locality, ConstRef kn) in if with_clean then Pfedit.delete_current_proof (); - Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); + CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r); definition_message id diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 23f1da1ba7..e5c756f564 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> - unit Lemmas.declaration_hook Ephemeron.key -> unit + unit Lemmas.declaration_hook CEphemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and abort the proof -- cgit v1.2.3 From 8d828a124d66a79b6e35c02097b05df252d1e1d4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Mar 2016 03:02:01 +0100 Subject: Moving Eauto to a simple ML file. --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8f8a19e5b..02cd819f4a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto (false,5) [] (Some []) + Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls -- cgit v1.2.3 From 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 14:42:51 +0100 Subject: Removing the registering of default values for generic arguments. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 97b9e95e10..61ada5cc8c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -146,7 +146,7 @@ module Tactic = Pcoq.Tactic type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) = - Genarg.create_arg None "function_rec_definition_loc" + Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) -- cgit v1.2.3 From d66fe71c93bc06f6006c64118deb1d5b01bf7487 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:01:23 +0100 Subject: Adding a universe argument to Pcoq.create_generic_entry. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61ada5cc8c..dbcdeb83ad 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -149,7 +149,7 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar Genarg.create_arg "function_rec_definition_loc" let function_rec_definition_loc = - Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) + Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) GEXTEND Gram GLOBAL: function_rec_definition_loc ; -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- plugins/funind/g_indfun.ml4 | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index dbcdeb83ad..4bd69b9fe7 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -16,8 +16,12 @@ open Constrexpr open Indfun_common open Indfun open Genarg +open Constrarg open Tacticals open Misctypes +open Pcoq.Prim +open Pcoq.Constr +open Pcoq.Tactic DECLARE PLUGIN "recdef_plugin" -- cgit v1.2.3 From 36e865119e5bb5fbaed14428fc89ecd4e96fb7be Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 18:27:39 +0100 Subject: Removing the special status of generic arguments defined by Coq itself. This makes the TACTIC EXTEND macro insensitive to Coq-defined arguments. They now have to be reachable in the ML code. Note that this has some consequences, as the previous macro was potentially mixing grammar entries and arguments as long as their name was the same. Now, each genarg comes with its grammar instead, so there is no way to abuse the macro. --- plugins/funind/g_indfun.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4bd69b9fe7..e93c395e3d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -94,7 +94,7 @@ let out_disjunctive = function | loc, IntroAction (IntroOrAndPattern l) -> (loc,l) | _ -> Errors.error "Disjunctive or conjunctive intro pattern expected." -ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END -- cgit v1.2.3