diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 26 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 8 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 7 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 138 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 136 | ||||
| -rw-r--r-- | plugins/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 15 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 26 | ||||
| -rw-r--r-- | plugins/funind/merge.ml | 37 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 32 |
12 files changed, 236 insertions, 197 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5f6d783598..bd5fb1d923 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclTHENLIST [ (* We first introduce the variables *) - tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps)); + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); (* Then the equation itself *) Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ @@ -1614,7 +1614,7 @@ let prove_principle_for_gen let hid = next_ident_away_in_goal (Id.of_string "prov") - hyps + (Id.Set.of_list hyps) in tclTHENLIST [ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 513fce2484..018b515170 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -11,7 +11,6 @@ open Tactics open Context.Rel.Declaration open Indfun_common open Functional_principles_proofs -open Misctypes module RelDecl = Context.Rel.Declaration @@ -40,7 +39,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | decl :: predicates -> (match Context.Rel.Declaration.get_name decl with | Name x -> - let id = Namegen.next_ident_away x avoid in + let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in Hashtbl.add tbl id x; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) @@ -286,7 +285,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let time2 = System.get_time () in *) (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) let new_princ_name = - next_ident_away_in_goal (Id.of_string "___________princ_________") [] + next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in let hook = Lemmas.mk_hook (hook new_principle_type) in @@ -339,13 +338,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) then (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = - 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' (EConstr.of_constr value)) in - (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value 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' (EConstr.of_constr value)) in + (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) + let univs = (snd (Evd.universe_context ~names:[] ~extensible:true evd')) in + let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in ignore( Declare.declare_constant name @@ -463,7 +463,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) : Safe_typing.private_constants definition_entry list = +let make_scheme evd (fas : (pconstant*Sorts.family) 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 @@ -500,7 +500,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd (Pretyping.interp_elimination_sort x) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x ) fas in @@ -674,7 +674,7 @@ let build_case_scheme fa = let scheme_type = EConstr.Unsafe.to_constr ((Typing.unsafe_type_of env sigma) (EConstr.of_constr scheme)) in let sorts = (fun (_,_,x) -> - Universes.new_sort_in_family (Pretyping.interp_elimination_sort x) + Universes.new_sort_in_family x ) fa in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 5a7ffe0590..2eb1b7935d 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -8,7 +8,6 @@ open Names open Term -open Misctypes val generate_functional_principle : Evd.evar_map ref -> @@ -37,8 +36,7 @@ val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (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 + (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list +val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 16d9f200f3..829556a71e 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -144,8 +144,7 @@ END let () = let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in - Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer (* TASSI: n'importe quoi ! *) VERNAC COMMAND EXTEND Function @@ -166,11 +165,11 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ - Ppconstr.pr_glob_sort s + Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg PRINTED BY pr_fun_scheme_arg -| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort(s) ] -> [ (princ_name,fun_name,s) ] +| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ] END diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 8cf5e8442d..e8e5bfccc1 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -34,10 +34,10 @@ type glob_context = (binder_type*glob_constr) list let rec solve_trivial_holes pat_as_term e = - match pat_as_term.CAst.v,e.CAst.v with + match DAst.get pat_as_term, DAst.get e with | GHole _,_ -> e | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> - CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) | _,_ -> pat_as_term (* @@ -120,13 +120,13 @@ let combine_args arg args = let ids_of_binder = function - | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] - | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in + let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: (if Id.Map.is_empty new_mapping then l @@ -137,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if Id.List.mem x_id (ids_of_binder bt) + if Id.Set.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l -let add_bt_names bt = List.append (ids_of_binder bt) +let add_bt_names bt = Id.Set.union (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || Id.List.mem id avoid + List.exists (is_free_in id) args || Id.Set.mem id avoid in let need_convert avoid bt = - List.exists (need_convert_id avoid) (ids_of_binder bt) + Id.Set.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) = match na with - | Name id when Id.List.mem id avoid -> + | Name id when Id.Set.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Id.Map.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:Id.t list) = + let next_bt_away bt (avoid:Id.Set.t) = match bt with | LetIn na -> let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in @@ -182,15 +182,15 @@ let apply_args ctxt body args = let new_avoid,new_ctxt',new_body,new_id = if need_convert_id avoid id then - let new_avoid = id::avoid in + let new_avoid = Id.Set.add id avoid in let new_id = Namegen.next_ident_away id new_avoid in - let new_avoid' = new_id :: new_avoid in + let new_avoid' = Id.Set.add new_id new_avoid in let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id else - id::avoid,ctxt',body,id + Id.Set.add id avoid,ctxt',body,id in let new_body = replace_var_by_term new_id arg new_body in let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in @@ -214,7 +214,7 @@ let apply_args ctxt body args = in (new_bt,t)::new_ctxt',new_body in - do_apply [] ctxt body args + do_apply Id.Set.empty ctxt body args let combine_app f args = @@ -361,7 +361,7 @@ 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.from_env env)); - match pat.CAst.v with + match DAst.get pat with | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env | PatCstr(c,patl,na) -> let Inductiveops.IndType(indf,indargs) = @@ -411,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env = -let rec pattern_to_term_and_type env typ = CAst.with_val (function +let rec pattern_to_term_and_type env typ = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar (Name id) -> mkGVar id @@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) + (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -480,7 +480,7 @@ let rec pattern_to_term_and_type env typ = CAst.with_val (function let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = observe (str " Entering : " ++ Printer.pr_glob_constr rt); let open CAst in - match rt.v with + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> (* do nothing (except changing type of course) *) mk_result [] rt avoid @@ -496,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = (mk_result [] [] avoid) in begin - match f.v with + match DAst.get f with | GLambda _ -> let rec aux t l = match l with | [] -> t - | u::l -> CAst.make @@ - match t.v with + | u::l -> DAst.make @@ + match DAst.get t with | GLambda(na,_,nat,b) -> GLetIn(na,u,None,aux b l) | _ -> @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) 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) (EConstr.of_constr rt_as_constr) in - let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in + let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -559,12 +559,12 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = match n with | Name id when List.exists (is_free_in id) args -> (* need to alpha-convert the name *) - let new_id = Namegen.next_ident_away id avoid in + let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in let new_avoid = id:: avoid in let new_b = replace_var_by_term id - (CAst.make @@ GVar id) + (DAst.make @@ GVar id) b in (Name new_id,new_b,new_avoid) @@ -626,7 +626,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = then the one corresponding to the value [t] and combine the two result *) - let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in @@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] + Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ_as_constr = EConstr.of_constr typ_as_constr in - let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in + let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in (* removing trivial holes *) let pat_as_term = solve_trivial_holes pat_as_term e in @@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -875,15 +875,23 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve { brl'_res with result = this_branch_res@brl'_res.result } -let is_res id = - try +let is_res r = match DAst.get r with +| GVar id -> + begin try String.equal (String.sub (Id.to_string id) 0 4) "_res" - with Invalid_argument _ -> false + with Invalid_argument _ -> false end +| _ -> false +let is_gr c gr = match DAst.get c with +| GRef (r, _) -> Globnames.eq_gr r gr +| _ -> false +let is_gvar c = match DAst.get c with +| GVar id -> true +| _ -> false let same_raw_term rt1 rt2 = - match CAst.(rt1.v, rt2.v) with + match DAst.get rt1, DAst.get rt2 with | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2 | GHole _, GHole _ -> true | _ -> false @@ -917,23 +925,24 @@ 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 let open CAst in - match rt.v with + match DAst.get rt with | GProd(n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin - match t with - | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id -> + match DAst.get t with + | GApp(res_rt ,args') when is_res res_rt -> begin - match args' with - | { v = GVar this_relname }::args' -> + let arg = List.hd args' in + match DAst.get arg with + | GVar this_relname -> (*i The next call to mk_rel_id is valid since we are constructing the graph Ensures by: obvious i*) let new_t = - mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt]) + mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt]) in let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in let new_env = Environ.push_rel (LocalAssum (n,t')) env in @@ -948,9 +957,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = | _ -> (* the first args is the name of the function! *) assert false end - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty; id ;rt]) + when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> + let loc1 = rt.CAst.loc in + let loc2 = eq_as_ref.CAst.loc in + let loc3 = id.CAst.loc in + let id = match DAst.get id with GVar id -> id | _ -> assert false in begin try observe (str "computing new type for eq : " ++ pr_glob_constr rt); @@ -985,10 +998,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let params,arg' = ((Util.List.chop nparam args')) in - let rt_typ = CAst.make @@ - GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None), + let rt_typ = DAst.make @@ + GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype false [] + (fun p -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr p)) params)@(Array.to_list (Array.make @@ -996,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (mkGHole ())))) in let eq' = - CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt]) + DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar 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.from_env env) eq' in @@ -1015,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype false [] + (id',Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc @@ -1065,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = mkGProd(n,t,new_b),id_to_exclude else new_b, Id.Set.add id id_to_exclude *) - | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) } - when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous + | GApp(eq_as_ref,[ty;rt1;rt2]) + when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous -> begin try @@ -1077,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = List.fold_left (fun acc (lhs,rhs) -> mkGProd(Anonymous, - mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc) + mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc) ) b l @@ -1135,14 +1148,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = then new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) else - CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude + DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude | _ -> anomaly (Pp.str "Should not have an anonymous function here.") (* We have renamed all the anonymous functions during alpha_renaming phase *) end | GLetIn(n,v,t,b) -> begin - let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in + let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in 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 @@ -1158,7 +1171,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) + | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(nal,(na,rto),t,b) -> @@ -1184,7 +1197,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* | Name id when Id.Set.mem id id_to_exclude -> *) (* new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *) (* | _ -> *) - CAst.make @@ GLetTuple(nal,(na,None),t,new_b), + DAst.make @@ GLetTuple(nal,(na,None),t,new_b), Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude') end @@ -1210,12 +1223,15 @@ let rebuild_cons env nb_args relname args crossed_types rt = TODO: Find a valid way to deal with implicit arguments here! *) -let rec compute_cst_params relnames params gt = CAst.with_val (function +let rec compute_cst_params relnames params gt = DAst.with_val (function | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params - | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames -> - compute_cst_params_from_app [] (params,rtl) | GApp(f,args) -> + begin match DAst.get f with + | GVar relname' when Id.Set.mem relname' relnames -> + compute_cst_params_from_app [] (params,args) + | _ -> List.fold_left (compute_cst_params relnames) params (f::args) + end | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b @@ -1232,10 +1248,10 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function raise (UserError(Some "compute_cst_params", str "Not handled case")) ) gt and compute_cst_params_from_app acc (params,rtl) = + let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl' - when Id.compare id id' == 0 -> + | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 003bb4e30d..0666ab4f1f 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -10,36 +10,36 @@ open Misctypes Some basic functions to rebuild glob_constr In each of them the location is Loc.ghost *) -let mkGRef ref = CAst.make @@ GRef(ref,None) -let mkGVar id = CAst.make @@ GVar(id) -let mkGApp(rt,rtl) = CAst.make @@ GApp(rt,rtl) -let mkGLambda(n,t,b) = CAst.make @@ GLambda(n,Explicit,t,b) -let mkGProd(n,t,b) = CAst.make @@ GProd(n,Explicit,t,b) -let mkGLetIn(n,b,t,c) = CAst.make @@ GLetIn(n,b,t,c) -let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl) -let mkGSort s = CAst.make @@ GSort(s) -let mkGHole () = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) -let mkGCast(b,t) = CAst.make @@ GCast(b,CastConv t) +let mkGRef ref = DAst.make @@ GRef(ref,None) +let mkGVar id = DAst.make @@ GVar(id) +let mkGApp(rt,rtl) = DAst.make @@ GApp(rt,rtl) +let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) +let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) +let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) +let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl) +let mkGSort s = DAst.make @@ GSort(s) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGCast(b,t) = DAst.make @@ GCast(b,CastConv t) (* Some basic functions to decompose glob_constrs These are analogous to the ones constrs *) let glob_decompose_prod = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args c = match DAst.get c with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod [] let glob_decompose_prod_or_letin = - let rec glob_decompose_prod args = function - | { CAst.v = GProd(n,k,t,b) } -> + let rec glob_decompose_prod args rt = match DAst.get rt with + | GProd(n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,rt in glob_decompose_prod [] @@ -58,10 +58,10 @@ let glob_decompose_prod_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,t)::args) b - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -70,12 +70,12 @@ let glob_decompose_prod_or_letin_n n = let rec glob_decompose_prod i args c = if i<=0 then args,c else - match c with - | { CAst.v = GProd(n,_,t,b) } -> + match DAst.get c with + | GProd(n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | { CAst.v = GLetIn(n,b,t,c) } -> + | GLetIn(n,b,t,c) -> glob_decompose_prod (i-1) ((n,Some b,t)::args) c - | rt -> args,rt + | _ -> args,c in glob_decompose_prod n [] @@ -83,10 +83,10 @@ let glob_decompose_prod_or_letin_n n = let glob_decompose_app = let rec decompose_rapp acc rt = (* msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *) - match rt with - | { CAst.v = GApp(rt,rtl) } -> + match DAst.get rt with + | GApp(rt,rtl) -> decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt - | rt -> rt,List.rev acc + | _ -> rt,List.rev acc in decompose_rapp [] @@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na = let change_vars = let rec change_vars mapping rt = - CAst.map_with_loc (fun ?loc -> function + DAst.map_with_loc (fun ?loc -> function | GRef _ as x -> x | GVar id -> let new_id = @@ -191,22 +191,22 @@ let change_vars = let rec alpha_pat excluded pat = let loc = pat.CAst.loc in - match pat.CAst.v with + match DAst.get pat with | PatVar Anonymous -> let new_id = Indfun_common.fresh_id excluded "_x" in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty | PatVar(Name id) -> if Id.List.mem id excluded then - let new_id = Namegen.next_ident_away id excluded in - (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in + (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty | PatCstr(constr,patl,na) -> let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty in @@ -219,7 +219,7 @@ let rec alpha_pat excluded pat = ([],new_excluded,map) patl in - (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map + (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map let alpha_patl excluded patl = let patl,new_excluded,map = @@ -238,7 +238,7 @@ let alpha_patl excluded patl = let raw_get_pattern_id pat acc = let rec get_pattern_id pat = - match pat.CAst.v with + match DAst.get pat with | PatVar(Anonymous) -> assert false | PatVar(Name id) -> [id] @@ -257,11 +257,11 @@ let get_pattern_id pat = raw_get_pattern_id pat [] let rec alpha_rt excluded rt = let loc = rt.CAst.loc in - let new_rt = CAst.make ?loc @@ - match rt.CAst.v with + let new_rt = DAst.make ?loc @@ + match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in + let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in @@ -276,7 +276,7 @@ let rec alpha_rt excluded rt = let new_c = alpha_rt excluded c in GLetIn(Anonymous,new_b,new_t,new_c) | GLambda(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let t,b = if Id.equal new_id id then t, b @@ -289,7 +289,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GLambda(Name new_id,k,new_t,new_b) | GProd(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let new_excluded = new_id::excluded in let t,b = if Id.equal new_id id @@ -302,7 +302,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GProd(Name new_id,k,new_t,new_b) | GLetIn(Name id,b,t,c) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let c = if Id.equal new_id id then c else change_vars (Id.Map.add id new_id Id.Map.empty) c @@ -320,7 +320,7 @@ let rec alpha_rt excluded rt = match na with | Anonymous -> (na::nal,excluded,mapping) | Name id -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in if Id.equal new_id id then na::nal,id::excluded,mapping @@ -377,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) = [is_free_in id rt] checks if [id] is a free variable in [rt] *) let is_free_in id = - let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function + let rec is_free_in x = DAst.with_loc_val (fun ?loc -> function | GRef _ -> false | GVar id' -> Id.compare id' id == 0 | GEvar _ -> false @@ -421,7 +421,7 @@ let is_free_in id = -let rec pattern_to_term pt = CAst.with_val (function +let rec pattern_to_term pt = DAst.with_val (function | PatVar Anonymous -> assert false | PatVar(Name id) -> mkGVar id @@ -448,8 +448,8 @@ let rec pattern_to_term pt = CAst.with_val (function let replace_var_by_term x_id term = - let rec replace_var_by_pattern x = CAst.map (function - | GVar id when Id.compare id x_id == 0 -> term.CAst.v + let rec replace_var_by_pattern x = DAst.map (function + | GVar id when Id.compare id x_id == 0 -> DAst.get term | GRef _ | GVar _ | GEvar _ @@ -522,11 +522,10 @@ exception NotUnifiable let rec are_unifiable_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -545,11 +544,10 @@ let are_unifiable pat1 pat2 = let rec eq_cases_pattern_aux = function | [] -> () - | eq::eqs -> - let open CAst in - match eq with - | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs - | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } -> + | (l, r) ::eqs -> + match DAst.get l, DAst.get r with + | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs + | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) -> if not (eq_constructor constructor2 constructor1) then raise NotUnifiable else @@ -569,7 +567,7 @@ let eq_cases_pattern pat1 pat2 = let ids_of_pat = - let rec ids_of_pat ids = CAst.with_val (function + let rec ids_of_pat ids = DAst.with_val (function | PatVar Anonymous -> ids | PatVar(Name id) -> Id.Set.add id ids | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl @@ -583,9 +581,9 @@ let id_of_name = function (* TODO: finish Rec caes *) let ids_of_glob_constr c = - let rec ids_of_glob_constr acc {loc; CAst.v = c} = + let rec ids_of_glob_constr acc c = let idof = id_of_name in - match c with + match DAst.get c with | GVar id -> id::acc | GApp (g,args) -> ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc @@ -610,7 +608,7 @@ let ids_of_glob_constr c = let zeta_normalize = - let rec zeta_normalize_term x = CAst.map (function + let rec zeta_normalize_term x = DAst.map (function | GRef _ | GVar _ | GEvar _ @@ -632,9 +630,9 @@ let zeta_normalize = zeta_normalize_term b ) | GLetIn(Name id,def,typ,b) -> - (zeta_normalize_term (replace_var_by_term id def b)).CAst.v + DAst.get (zeta_normalize_term (replace_var_by_term id def b)) | GLetIn(Anonymous,def,typ,b) -> - (zeta_normalize_term b).CAst.v + DAst.get (zeta_normalize_term b) | GLetTuple(nal,(na,rto),def,b) -> GLetTuple(nal, (na,Option.map zeta_normalize_term rto), @@ -670,19 +668,19 @@ let zeta_normalize = let expand_as = - let rec add_as map ({loc; CAst.v = pat } as rt) = - match pat with + let rec add_as map rt = + match DAst.get rt with | PatVar _ -> map | PatCstr(_,patl,Name id) -> Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl) | PatCstr(_,patl,_) -> List.fold_left add_as map patl in - let rec expand_as map = CAst.map (function + let rec expand_as map = DAst.map (function | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt | GVar id as rt -> begin try - (Id.Map.find id map).CAst.v + DAst.get (Id.Map.find id map) with Not_found -> rt end | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args) @@ -723,7 +721,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas (* then we map [rt] to replace the implicit holes by their values *) let rec change rt = - match rt.CAst.v with + match DAst.get rt with | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *) ( try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *) @@ -743,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -765,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8769f56688..dab094f913 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -191,7 +191,7 @@ let error msg = user_err Pp.(str msg) let is_rec names = let names = List.fold_right Id.Set.add names Id.Set.empty in let check_id id names = Id.Set.mem id names in - let rec lookup names gt = match gt.CAst.v with + let rec lookup names gt = match DAst.get gt with | GVar(id) -> check_id id names | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ -> false | GCast(b,_) -> lookup names b diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index f4f9ba2bbb..76fcd5ec87 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -12,7 +12,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = () -let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid +let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid) let fresh_name avoid s = Name (fresh_id avoid s) @@ -66,7 +66,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -80,7 +80,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get rt with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in @@ -549,3 +549,12 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +(* We only "purify" on exceptions *) +let funind_purify f x = + let st = Vernacentries.freeze_interp_state `No in + try f x + with e -> + let e = CErrors.push e in + Vernacentries.unfreeze_interp_state st; + Exninfo.iraise e diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 2e2ced790e..d41abee87e 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -123,3 +123,5 @@ type tcc_lemma_value = | Undefined | Value of Term.constr | Not_needed + +val funind_purify : ('a -> 'b) -> ('a -> 'b) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8dea6c90f5..93317fce1b 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -131,9 +131,9 @@ let generate_type evd g_to_f f graph i = | Name id -> Some id | Anonymous -> None in - let named_ctxt = List.map_filter filter fun_ctxt in + let named_ctxt = Id.Set.of_list (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 + let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in (*i @@ -189,7 +189,7 @@ let rec generate_fresh_id x avoid i = if i == 0 then [] else - let id = Namegen.next_ident_away_in_goal x avoid in + let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in id::(generate_fresh_id x (id::avoid) (pred i)) @@ -239,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes environment and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -396,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -406,7 +406,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -570,6 +570,11 @@ let rec reflexivity_with_destruct_cases g = with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in + let my_inj_flags = Some { + Equality.keep_proof_equalities = false; + injection_in_context = false; (* for compatibility, necessary *) + injection_pattern_l2r_order = false; (* probably does not matter; except maybe with dependent hyps *) + } in let discr_inject = Tacticals.onAllHypsAndConcl ( fun sc g -> @@ -580,8 +585,8 @@ let rec reflexivity_with_destruct_cases g = | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind -> if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g - else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g + else if Equality.injectable (pf_env g) (project g) ~keep_proofs:None t1 t2 + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp my_inj_flags None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) @@ -759,7 +764,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let funs = Array.of_list funs and graphs = Array.of_list graphs in let map (c, u) = mkConstU (c, EInstance.make u) in let funs_constr = Array.map map funs in - States.with_state_protection_on_exception + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> let env = Global.env () in let evd = ref (Evd.from_env env) in @@ -797,7 +803,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( (fun entry -> (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type )) ) - (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs)) + (make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs)) ) ) in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 3ae9221903..77c26f8ce6 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -64,8 +64,8 @@ let string_of_name = id_of_name %> Id.to_string (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *) let isVarf f x = - match x with - | { CAst.v = GVar x } -> Id.equal x f + match DAst.get x with + | GVar x -> Id.equal x f | _ -> false (** [ident_global_exist id] returns true if identifier [id] is linked @@ -491,38 +491,38 @@ exception NoMerge let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 -> let _ = prstr "\nICI1!\n" in let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args) + DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args) | GApp(f1, arr1), GApp(f2,arr2) -> raise NoMerge | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let lnk = Array.append shift.lnk1 shift.lnk2 in - match CAst.(c1.v, c2.v) with + match DAst.get c1, DAst.get c2 with | GApp(f1, arr1), GApp(f2,arr2) -> let args = filter_shift_stable lnk (arr1 @ arr2) in - CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args) + DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args) (* FIXME: what if the function appears in the body of the let? *) | GLetIn(nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _, GLetIn(nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - CAst.make @@ GLetIn(nme,bdy,typ,newtrm) + DAst.make @@ GLetIn(nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge @@ -533,16 +533,18 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let rec merge_rec_hyps shift accrec (ltyp:(Name.t * glob_constr option * glob_constr option) list) filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list = + let is_app c = match DAst.get c with GApp _ -> true | _ -> false in let mergeonehyp t reldecl = match reldecl with - | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind)) + | (nme,x,Some ind) when is_app ind -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable) | (nme,Some _,None) -> error "letins with recursive calls not treated yet" | (nme,None,Some _) -> assert false | (nme,None,None) | (nme,Some _,Some _) -> assert false in + let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in match ltyp with | [] -> [] - | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f -> + | (nme,None,Some t) :: lt when is_app t -> let rechyps = List.map (mergeonehyp t) accrec in rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable @@ -553,12 +555,13 @@ let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift = let find_app (nme:Id.t) ltyp = + let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in try ignore (List.map (fun x -> match x with - | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0) + | _,None,Some c when is_app c -> raise (Found 0) | _ -> ()) ltyp); false @@ -617,7 +620,7 @@ let rec merge_types shift accrec1 rechyps , concl | (nme,None, Some t1)as e ::lt1 -> - (match t1.CAst.v with + (match DAst.get t1 with | GApp(f,carr) when isVarf ind1name f -> merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2 | _ -> @@ -764,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in + Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -848,8 +851,8 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> let t = EConstr.of_constr t in - let traw = Detyping.detype false [] (Global.env()) Evd.empty t in - CAst.make @@ GProd (nme,Explicit,traw,t2) + let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in + DAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d3eccb58d7..76f859ed72 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,13 +115,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in + let ids = Id.Set.of_list ids in List.fold_right - (fun id acc -> next_global_ident_away id (acc@ids)::acc) + (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc) idl [] +let next_ident_away_in_goal ids avoid = + next_ident_away_in_goal ids (Id.Set.of_list avoid) + let compute_renamed_type gls c = - rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) [] + rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" @@ -190,15 +194,15 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) = in let env = Environ.push_rel_context context (Global.env ()) in let glob_body = - CAst.make @@ + DAst.make @@ GCases (RegularStyle,None, - [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l), + [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l), (Anonymous,None)], - [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), - [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous], + [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1), + [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous], Anonymous)], - CAst.make @@ GVar v_id)]) + DAst.make @@ GVar v_id)]) in let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context @@ -1288,8 +1292,8 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None - | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque + | Declarations.Undef _ -> Vernacexpr.Opaque | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = @@ -1302,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unamed theorem.") in - let na = next_global_ident_away name [] in + let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = @@ -1543,7 +1547,10 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + let functional_ref = + let ctx = (snd (Evd.universe_context ~names:[] ~extensible:true evm)) in + declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res + in (* Refresh the global universes, now including those of _F *) let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in @@ -1588,7 +1595,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num spc () ++ str"is defined" ) ) in - States.with_state_protection_on_exception (fun () -> + (* XXX STATE Why do we need this... why is the toplevel protection not enought *) + funind_purify (fun () -> com_terminate tcc_lemma_name tcc_lemma_constr |