From 5af486406e366bf23558311a7367e573c617e078 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Fri, 5 Apr 2019 12:18:49 +0200 Subject: [PATCH] Remove calls to global env in Inductiveops --- interp/constrextern.ml | 12 +- interp/constrintern.ml | 31 ++--- interp/notation_ops.ml | 5 +- library/goptions.ml | 12 +- library/goptions.mli | 4 +- plugins/cc/cctac.ml | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/firstorder/formula.ml | 8 +- plugins/firstorder/sequent.ml | 2 +- plugins/funind/glob_term_to_relation.ml | 6 +- plugins/funind/glob_termops.ml | 2 +- plugins/ltac/tauto.ml | 18 ++- plugins/ssr/ssrequality.ml | 4 +- pretyping/cases.ml | 8 +- pretyping/classops.ml | 4 +- pretyping/detyping.ml | 14 +-- pretyping/detyping.mli | 4 +- pretyping/evarsolve.ml | 12 +- pretyping/glob_ops.ml | 8 +- pretyping/glob_ops.mli | 2 +- pretyping/inductiveops.ml | 143 +++++++++++------------- pretyping/inductiveops.mli | 49 +++++--- pretyping/pretyping.ml | 2 +- pretyping/retyping.ml | 2 +- tactics/contradiction.ml | 12 +- tactics/elim.ml | 9 +- tactics/equality.ml | 13 ++- tactics/hints.ml | 4 +- tactics/hipattern.ml | 105 +++++++++-------- tactics/hipattern.mli | 8 +- tactics/tactics.ml | 13 ++- vernac/indschemes.ml | 4 +- 32 files changed, 267 insertions(+), 257 deletions(-) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 24b1362e6d89..b89b6b57653b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -212,7 +212,7 @@ let encode_record r = module PrintingRecordRecord = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Record" let title = "Types leading to pretty-printing using record notation: " let member_message s b = @@ -224,7 +224,7 @@ module PrintingRecordRecord = module PrintingRecordConstructor = PrintingInductiveMake (struct - let encode = encode_record + let encode _env = encode_record let field = "Constructor" let title = "Types leading to pretty-printing using constructor form: " let member_message s b = @@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l let add_patt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l let add_cpatt_for_params ind l = if !Flags.in_debugger then l else - Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l + Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@ let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in - let nb_params = Inductiveops.inductive_nparams ind in + let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in List.exists (fun (_,impls) -> (List.length impls >= nb_params) && let params,args = Util.List.chop nb_params impls in @@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and not explicit application. *) - if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then + if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), []) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d4555707c482..808dd225aff0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -658,7 +658,7 @@ let terms_of_binders bl = | PatCstr (c,l,_) -> let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in - let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in + let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> @@ -1212,10 +1212,10 @@ let check_or_pat_variables loc ids idsl = @return if letin are included *) let check_constructor_length env loc cstr len_pl pl0 = let n = len_pl + List.length pl0 in - if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else - (Int.equal n (Inductiveops.constructor_nalldecls cstr) || + if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls env cstr) || (error_wrong_numarg_constructor ?loc env cstr - (Inductiveops.constructor_nrealargs cstr))) + (Inductiveops.constructor_nrealargs env cstr))) open Declarations @@ -1241,9 +1241,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with have been given in the "explicit" arguments, which come from a "@C args" notation or from a custom user notation *) let pl' = insert_local_defs_in_pattern cstr pl in - let maxargs = Inductiveops.constructor_nalldecls cstr in + let maxargs = Inductiveops.constructor_nalldecls env cstr in if List.length pl' + List.length args > maxargs then - error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr); + error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr); (* Two possibilities: either the args are given with explict variables for local definitions, then we give the explicit args extended with local defs, so that there is nothing more to be @@ -1273,15 +1273,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 in aux 0 (impl_list,pl2) let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.constructor_nallargs c in - let nargs' = Inductiveops.constructor_nalldecls c in + let nargs = Inductiveops.constructor_nallargs env c in + let nargs' = Inductiveops.constructor_nalldecls env c in let impls_st = implicits_of_global (ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor ?loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let nallargs = inductive_nallargs_env env c in - let nalldecls = inductive_nalldecls_env env c in + let nallargs = inductive_nallargs env c in + let nalldecls = inductive_nalldecls env c in let impls_st = implicits_of_global (IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive ?loc env c) nallargs nalldecls impls_st len_pl1 pl2 @@ -1289,8 +1289,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 = (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind in + then Inductiveops.inductive_nparamdecls (Global.env()) ind + else Inductiveops.inductive_nparams (Global.env()) ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in List.iter (fun c -> match DAst.get c with @@ -1310,10 +1310,11 @@ let find_constructor loc add_params ref = in cstr, match add_params with | Some nb_args -> + let env = Global.env () in let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) - then Inductiveops.inductive_nparamdecls ind - else Inductiveops.inductive_nparams ind + if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr) + then Inductiveops.inductive_nparamdecls env ind + else Inductiveops.inductive_nparams env ind in List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1f1cf4506f9e..9801e56ca136 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function | GApp (t, l) -> begin match DAst.get t with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in let _,l = List.chop nparams l in PatCstr (cstr, List.map pat_binder_of_term l, Anonymous) | _ -> raise No_match @@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) alp, add_env alp sigma var (DAst.make @@ GVar id) let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c = - let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in + let env = Global.env () in + let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in try (* If already bound to a binder, unify the term and the binder *) let patl' = Id.List.assoc var binders in diff --git a/library/goptions.ml b/library/goptions.ml index 1b907fd96685..b9c1802a7273 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -57,7 +57,7 @@ module MakeTable = type key val compare : t -> t -> int val table : (string * key table_of_A) list ref - val encode : key -> t + val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -111,10 +111,10 @@ module MakeTable = class table_of_A () = object - method add x = add_option (A.encode x) - method remove x = remove_option (A.encode x) + method add x = add_option (A.encode (Global.env()) x) + method remove x = remove_option (A.encode (Global.env()) x) method mem x = - let y = A.encode x in + let y = A.encode (Global.env()) x in let answer = MySet.mem y !t in Feedback.msg_info (A.member_message y answer) method print = print_table A.title A.printer !t @@ -142,7 +142,7 @@ struct type key = string let compare = String.compare let table = string_table - let encode x = x + let encode _env x = x let subst _ x = x let printer = str let key = A.key @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : qualid -> t + val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name diff --git a/library/goptions.mli b/library/goptions.mli index b91553bf3ccf..9925eb9e7b98 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,8 +89,8 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : qualid -> t - val subst : substitution -> t -> t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name val title : string diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 50fc2448fc3e..0e3b9fc2b65f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -67,7 +67,7 @@ let rec decompose_term env sigma t= let canon_mind = MutInd.make1 (MutInd.canonical mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=constructor_nallargs_env env (canon_ind,i_con) in + let nargs=constructor_nallargs env (canon_ind,i_con) in Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index c9cfd7436246..9db7c8d8d327 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args = and extract_case env sg mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = constructors_nrealargs_env env ip in + let ni = constructors_nrealargs env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 56b3dc97cfd6..4b7bc707d6cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t let kind_of_formula env sigma term = let normalize = special_nf env sigma in let cciterm = special_whd env sigma term in - match match_with_imp_term sigma cciterm with + match match_with_imp_term env sigma cciterm with Some (a,b)-> Arrow (a, pop b) |_-> - match match_with_forall_term sigma cciterm with + match match_with_forall_term env sigma cciterm with Some (_,a,b)-> Forall (a, b) |_-> - match match_with_nodep_ind sigma cciterm with + match match_with_nodep_ind env sigma cciterm with Some (i,l,n)-> let ind,u=EConstr.destInd sigma i in let u = EConstr.EInstance.kind sigma u in @@ -111,7 +111,7 @@ let kind_of_formula env sigma term = else Or((ind,u),l,is_trivial) | _ -> - match match_with_sigma_type sigma cciterm with + match match_with_sigma_type env sigma cciterm with Some (i,l)-> let (ind, u) = EConstr.destInd sigma i in let u = EConstr.EInstance.kind sigma u in diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 01b18e2f30e6..9f2ceb2c28b2 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -188,7 +188,7 @@ let empty_seq depth= let expand_constructor_hints = List.map_append (function | GlobRef.IndRef ind -> - List.init (Inductiveops.nconstructors ind) + List.init (Inductiveops.nconstructors (Global.env()) ind) (fun i -> GlobRef.ConstructRef (ind,i+1)) | gr -> [gr]) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 275b58f0aaaa..45a4e6184690 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) construct in @@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl = let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) in - cases_pattern_of_glob_constr Anonymous pat_as_term + cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term ) ind.Declarations.mind_consnames @@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 13ff19a46b9f..7b758da8e876 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function mkGVar id | PatCstr(constr,patternl,_) -> let cst_narg = - Inductiveops.constructor_nallargs_env + Inductiveops.constructor_nallargs (Global.env ()) constr in diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4c65445b895e..d1951cc18d16 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings] (** Test *) let is_empty _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> - if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail + if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail (* Strictly speaking, this exceeds the propositional fragment as it matches also equality types (and solves them if a reflexivity) *) let is_unit_or_eq _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in - if test sigma (assoc_var "X1" ist) then idtac else fail + if test genv sigma (assoc_var "X1" ist) then idtac else fail let bugged_is_binary sigma t = isApp sigma t && @@ -121,23 +123,25 @@ let bugged_is_binary sigma t = (** Dealing with conjunction *) let is_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let ind = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) && - is_conjunction sigma + is_conjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode ind then idtac else fail let flatten_contravariant_conj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_conjunction sigma + match match_with_conjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with @@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist = (** Dealing with disjunction *) let is_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let t = assoc_var "X1" ist in if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) && - is_disjunction sigma + is_disjunction genv sigma ~strict:flags.strict_in_hyp_and_ccl ~onlybinary:flags.binary_mode t then idtac else fail let flatten_contravariant_disj _ ist = + Proofview.tclENV >>= fun genv -> Proofview.tclEVARMAP >>= fun sigma -> let flags = assoc_flags ist in let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in let hyp = assoc_var "id" ist in - match match_with_disjunction sigma + match match_with_disjunction genv sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index a7a3fee94244..4433f2fce7ce 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl = let sigma, rs2 = loop d sigma s a.(1) rs 0 in let s, sigma = sr sigma 1 in loop d sigma s a.(0) rs2 0 - | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None -> + | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None -> let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in - let np = Inductiveops.inductive_nparamdecls ind in + let np = Inductiveops.inductive_nparamdecls env ind in let indu = (ind, EConstr.EInstance.kind sigma u) in let ind_ct = Inductiveops.type_of_constructors env indu in let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index e22368d5e54e..d7a6c4c83257 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -284,7 +284,7 @@ let rec find_row_ind = function let inductive_template env sigma tmloc ind = let sigma, indu = Evd.fresh_inductive_instance env sigma ind in - let arsign = inductive_alldecls_env env indu in + let arsign = inductive_alldecls env indu in let indu = on_snd EInstance.make indu in let hole_source i = match tmloc with | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i) @@ -313,7 +313,7 @@ let try_find_ind env sigma typ realnames = | Some names -> names | None -> let ind = fst (fst (dest_ind_family indf)) in - List.make (inductive_nrealdecls ind) Anonymous in + List.make (inductive_nrealdecls env ind) Anonymous in IsInd (typ,ind,names) let inh_coerce_to_ind env sigma0 loc ty tyi = @@ -1796,7 +1796,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc | App (f,v) when isConstruct sigma f -> let cstr,u = destConstruct sigma f in - let n = constructor_nrealargs_env !!env cstr in + let n = constructor_nrealargs !!env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_right_map reveal_pattern l acc in DAst.make (PatCstr (cstr,l,Anonymous)), acc @@ -1929,7 +1929,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in - let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in + let nrealargs_ctxt = inductive_nrealdecls env0 ind in let arsign, inds = get_arity env0 indf' in let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in let realnal = diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 02038190517a..90ce1cc59428 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -287,7 +287,7 @@ let get_coercion_constructor env coe = let red x = fst (Reductionops.whd_all_stack env evd x) in match EConstr.kind evd (red (mkNamed coe.coe_value)) with | Constr.Construct (c, _) -> - c, Inductiveops.constructor_nrealargs c -1 + c, Inductiveops.constructor_nrealargs env c -1 | _ -> raise Not_found let lookup_pattern_path_between env (s,t) = @@ -442,7 +442,7 @@ module CoercionPrinting = struct type t = coe_typ let compare = GlobRef.Ordered.compare - let encode = coercion_of_reference + let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5003d0eec6ee..eaa573633674 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -145,9 +145,9 @@ let add_name_opt na b t (nenv, env) = (****************************************************************************) (* Tools for printing of Cases *) -let encode_inductive r = +let encode_inductive env r = let indsp = Nametab.global_inductive r in - let constr_lengths = constructors_nrealargs indsp in + let constr_lengths = constructors_nrealargs env indsp in (indsp,constr_lengths) (* Parameterization of the translation from constr to ast *) @@ -159,15 +159,15 @@ let has_two_constructors lc = let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1 -let encode_bool ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_bool env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (has_two_constructors lc) then user_err ?loc ~hdr:"encode_if" (str "This type has not exactly two constructors."); x -let encode_tuple ({CAst.loc} as r) = - let (x,lc) = encode_inductive r in +let encode_tuple env ({CAst.loc} as r) = + let (x,lc) = encode_inductive env r in if not (isomorphic_to_tuple lc) then user_err ?loc ~hdr:"encode_tuple" (str "This type cannot be seen as a tuple type."); @@ -175,7 +175,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : qualid -> inductive + val encode : Environ.env -> qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 425fd5096e71..1a8e97efb8eb 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -87,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.qualid -> Names.inductive + val encode : Environ.env -> Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -95,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.qualid -> Names.inductive + val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6d2d07d1dc66..4a941a68b1ae 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1203,17 +1203,17 @@ exception CannotProject of evar_map * EConstr.existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = +let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect evd t in match EConstr.kind evd f with | Construct ((ind,_),u) -> - let n = Inductiveops.inductive_nparams ind in + let n = Inductiveops.inductive_nparams env ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false evd k g) params - | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args - | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 + Array.for_all (is_constrainable_in false env evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false env evd k g) args + | Prod (na,t1,t2) -> is_constrainable_in false env evd k g t1 && is_constrainable_in false env evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels @@ -1238,7 +1238,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r | None -> (* t is an instance for a proper variable; we filter it along *) (* the free variables allowed to occur *) - (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t + (not force || noccur_evar env evd ev t) && is_constrainable_in true env evd k (ev,(fv_rels,fv_ids)) t exception EvarSolvedOnTheFly of evar_map * EConstr.constr diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 82e42d41becf..6da168711c16 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -492,7 +492,7 @@ let is_gvar id c = match DAst.get c with | GVar id' -> Id.equal id id' | _ -> false -let rec cases_pattern_of_glob_constr na c = +let rec cases_pattern_of_glob_constr env na c = (* Forcing evaluation to ensure that the possible raising of Not_found is not delayed *) let c = DAst.force c in @@ -509,14 +509,14 @@ let rec cases_pattern_of_glob_constr na c = | GApp (c, l) -> begin match DAst.get c with | GRef (ConstructRef cstr,_) -> - let nparams = Inductiveops.inductive_nparams (fst cstr) in + let nparams = Inductiveops.inductive_nparams env (fst cstr) in let _,l = List.chop nparams l in - PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na) | _ -> raise Not_found end | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous -> (* A canonical encoding of aliases *) - DAst.get (cases_pattern_of_glob_constr na' b) + DAst.get (cases_pattern_of_glob_constr env na' b) | _ -> raise Not_found ) c diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 47c65c2a7249..df902a8fa77d 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -94,7 +94,7 @@ val map_pattern : (glob_constr -> glob_constr) -> Evaluation is forced. Take the current alias as parameter, @raise Not_found if translation is impossible *) -val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g +val cases_pattern_of_glob_constr : Environ.env -> Name.t -> 'a glob_constr_g -> 'a cases_pattern_g val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 678aebfbe6e7..b1c98da2c74d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -112,162 +112,145 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = (* Number of constructors *) -let nconstructors ind = - let (_,mip) = Global.lookup_inductive ind in - Array.length mip.mind_consnames - -let nconstructors_env env ind = +let nconstructors env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in Array.length mip.mind_consnames -(* Arity of constructors excluding parameters, excluding local defs *) +let nconstructors_env env ind = nconstructors env ind +[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] -let constructors_nrealargs ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealargs +(* Arity of constructors excluding parameters, excluding local defs *) -let constructors_nrealargs_env env ind = +let constructors_nrealargs env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs -(* Arity of constructors excluding parameters, including local defs *) +let constructors_nrealargs_env env ind = constructors_nrealargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] -let constructors_nrealdecls ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealdecls +(* Arity of constructors excluding parameters, including local defs *) -let constructors_nrealdecls_env env ind = +let constructors_nrealdecls env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls +let constructors_nrealdecls_env env ind = constructors_nrealdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] + (* Arity of constructors including parameters, excluding local defs *) -let constructor_nallargs (indsp,j) = - let (mib,mip) = Global.lookup_inductive indsp in +let constructor_nallargs env (ind,j) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs.(j-1) + mib.mind_nparams -let constructor_nallargs_env env ((kn,i),j) = - let mib = Environ.lookup_mind kn env in - let mip = mib.mind_packets.(i) in - mip.mind_consnrealargs.(j-1) + mib.mind_nparams +let constructor_nallargs_env env (indsp,j) = constructor_nallargs env (indsp,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] (* Arity of constructors including params, including local defs *) -let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *) - let (mib,mip) = Global.lookup_inductive indsp in +let constructor_nalldecls env (ind,j) = (* TOCHANGE en decls *) + let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) -let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *) - let mib = Environ.lookup_mind kn env in - let mip = mib.mind_packets.(i) in - mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) +let constructor_nalldecls_env env (indsp,j) = constructor_nalldecls env (indsp,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] (* Arity of constructors excluding params, excluding local defs *) -let constructor_nrealargs (ind,j) = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealargs.(j-1) - -let constructor_nrealargs_env env (ind,j) = +let constructor_nrealargs env (ind,j) = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealargs.(j-1) -(* Arity of constructors excluding params, including local defs *) +let constructor_nrealargs_env env (ind,j) = constructor_nrealargs env (ind,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] -let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *) - let (_,mip) = Global.lookup_inductive ind in - mip.mind_consnrealdecls.(j-1) +(* Arity of constructors excluding params, including local defs *) -let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *) +let constructor_nrealdecls env (ind,j) = (* TOCHANGE en decls *) let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_consnrealdecls.(j-1) -(* Length of arity, excluding params, excluding local defs *) +let constructor_nrealdecls_env env (ind,j) = constructor_nrealdecls env (ind,j) +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] -let inductive_nrealargs ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_nrealargs +(* Length of arity, excluding params, excluding local defs *) -let inductive_nrealargs_env env ind = +let inductive_nrealargs env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_nrealargs -(* Length of arity, excluding params, including local defs *) +let inductive_nrealargs_env env ind = inductive_nrealargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] -let inductive_nrealdecls ind = - let (_,mip) = Global.lookup_inductive ind in - mip.mind_nrealdecls +(* Length of arity, excluding params, including local defs *) -let inductive_nrealdecls_env env ind = +let inductive_nrealdecls env ind = let (_,mip) = Inductive.lookup_mind_specif env ind in mip.mind_nrealdecls -(* Full length of arity (w/o local defs) *) +let inductive_nrealdecls_env env ind = inductive_nrealdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] -let inductive_nallargs ind = - let (mib,mip) = Global.lookup_inductive ind in - mib.mind_nparams + mip.mind_nrealargs +(* Full length of arity (w/o local defs) *) -let inductive_nallargs_env env ind = +let inductive_nallargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams + mip.mind_nrealargs -(* Length of arity (w/o local defs) *) +let inductive_nallargs_env env ind = inductive_nallargs env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] -let inductive_nparams ind = - let (mib,mip) = Global.lookup_inductive ind in - mib.mind_nparams +(* Length of arity (w/o local defs) *) -let inductive_nparams_env env ind = +let inductive_nparams env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams -(* Length of arity (with local defs) *) +let inductive_nparams_env env ind = inductive_nparams env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] -let inductive_nparamdecls ind = - let (mib,mip) = Global.lookup_inductive ind in - Context.Rel.length mib.mind_params_ctxt +(* Length of arity (with local defs) *) -let inductive_nparamdecls_env env ind = +let inductive_nparamdecls env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in Context.Rel.length mib.mind_params_ctxt -(* Full length of arity (with local defs) *) +let inductive_nparamdecls_env env ind = inductive_nparamdecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] -let inductive_nalldecls ind = - let (mib,mip) = Global.lookup_inductive ind in - Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls +(* Full length of arity (with local defs) *) -let inductive_nalldecls_env env ind = +let inductive_nalldecls env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls -(* Others *) +let inductive_nalldecls_env env ind = inductive_nalldecls env ind +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] -let inductive_paramdecls (ind,u) = - let (mib,mip) = Global.lookup_inductive ind in - Inductive.inductive_paramdecls (mib,u) +(* Others *) -let inductive_paramdecls_env env (ind,u) = +let inductive_paramdecls env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in Inductive.inductive_paramdecls (mib,u) -let inductive_alldecls (ind,u) = - let (mib,mip) = Global.lookup_inductive ind in - Vars.subst_instance_context u mip.mind_arity_ctxt +let inductive_paramdecls_env env (ind,u) = inductive_paramdecls env (ind,u) +[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"] -let inductive_alldecls_env env (ind,u) = +let inductive_alldecls env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in Vars.subst_instance_context u mip.mind_arity_ctxt -let constructor_has_local_defs (indsp,j) = - let (mib,mip) = Global.lookup_inductive indsp in +let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u) +[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] + +let constructor_has_local_defs env (indsp,j) = + let (mib,mip) = Inductive.lookup_mind_specif env indsp in let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in not (Int.equal l1 l2) -let inductive_has_local_defs ind = - let (mib,mip) = Global.lookup_inductive ind in +let inductive_has_local_defs env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in let l2 = mib.mind_nparams + mip.mind_nrealargs in not (Int.equal l1 l2) diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index c74bbfe98bc8..cfc650938ea7 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -61,70 +61,85 @@ val mis_nf_constructor_type : (** {6 Extract information from an inductive name} *) (** @return number of constructors *) -val nconstructors : inductive -> int +val nconstructors : env -> inductive -> int val nconstructors_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"] (** @return arity of constructors excluding parameters, excluding local defs *) -val constructors_nrealargs : inductive -> int array +val constructors_nrealargs : env -> inductive -> int array val constructors_nrealargs_env : env -> inductive -> int array +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"] (** @return arity of constructors excluding parameters, including local defs *) -val constructors_nrealdecls : inductive -> int array +val constructors_nrealdecls : env -> inductive -> int array val constructors_nrealdecls_env : env -> inductive -> int array +[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"] (** @return the arity, excluding params, excluding local defs *) -val inductive_nrealargs : inductive -> int +val inductive_nrealargs : env -> inductive -> int val inductive_nrealargs_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"] (** @return the arity, excluding params, including local defs *) -val inductive_nrealdecls : inductive -> int +val inductive_nrealdecls : env -> inductive -> int val inductive_nrealdecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"] (** @return the arity, including params, excluding local defs *) -val inductive_nallargs : inductive -> int +val inductive_nallargs : env -> inductive -> int val inductive_nallargs_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"] (** @return the arity, including params, including local defs *) -val inductive_nalldecls : inductive -> int +val inductive_nalldecls : env -> inductive -> int val inductive_nalldecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"] (** @return nb of params without local defs *) -val inductive_nparams : inductive -> int +val inductive_nparams : env -> inductive -> int val inductive_nparams_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"] (** @return nb of params with local defs *) -val inductive_nparamdecls : inductive -> int +val inductive_nparamdecls : env -> inductive -> int val inductive_nparamdecls_env : env -> inductive -> int +[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"] (** @return params context *) -val inductive_paramdecls : pinductive -> Constr.rel_context +val inductive_paramdecls : env -> pinductive -> Constr.rel_context val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context +[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecl"] (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> Constr.rel_context +val inductive_alldecls : env -> pinductive -> Constr.rel_context val inductive_alldecls_env : env -> pinductive -> Constr.rel_context +[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"] (** {7 Extract information from a constructor name} *) (** @return param + args without letin *) -val constructor_nallargs : constructor -> int +val constructor_nallargs : env -> constructor -> int val constructor_nallargs_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"] (** @return param + args with letin *) -val constructor_nalldecls : constructor -> int +val constructor_nalldecls : env -> constructor -> int val constructor_nalldecls_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"] (** @return args without letin *) -val constructor_nrealargs : constructor -> int +val constructor_nrealargs : env -> constructor -> int val constructor_nrealargs_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"] (** @return args with letin *) -val constructor_nrealdecls : constructor -> int +val constructor_nrealdecls : env -> constructor -> int val constructor_nrealdecls_env : env -> constructor -> int +[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"] (** Is there local defs in params or args ? *) -val constructor_has_local_defs : constructor -> bool -val inductive_has_local_defs : inductive -> bool +val constructor_has_local_defs : env -> constructor -> bool +val inductive_has_local_defs : env -> inductive -> bool val allowed_sorts : env -> inductive -> Sorts.family list diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e29672b6bc19..0f7676cd1929 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -644,7 +644,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env | None -> [] | Some ty -> let ((ind, i), u) = destConstruct sigma fj.uj_val in - let npars = inductive_nparams ind in + let npars = inductive_nparams !!env ind in if Int.equal npars 0 then [] else try diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 20120f4182ea..38e254a5b42c 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -121,7 +121,7 @@ let retype ?(polyprop=true) sigma = Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in - let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in + let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in let t = betazetaevar_applist sigma n p realargs in (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with | Prod _ -> whd_beta sigma (applist (t, [c])) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 3ff2e3852d7b..d9d3764b2af2 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -67,17 +67,17 @@ let contradiction_context = let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in - if is_empty_type sigma typ then + if is_empty_type env sigma typ then simplest_elim (mkVar id) else match EConstr.kind sigma typ with - | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = match_with_unit_or_eq_type sigma t in + | Prod (na,t,u) when is_empty_type env sigma u -> + let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> let hd,args = decompose_app sigma t in let (ind,_ as indu) = destInd sigma hd in - let nparams = Inductiveops.inductive_nparams_env env ind in + let nparams = Inductiveops.inductive_nparams env ind in let params = Util.List.firstn nparams args in let p = applist ((mkConstructUi (indu,1)), params) in (* Checking on the fly that it type-checks *) @@ -103,7 +103,7 @@ let contradiction_context = let is_negation_of env sigma typ t = match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,t,u) -> - is_empty_type sigma u && is_conv_leq env sigma typ t + is_empty_type env sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = @@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) = let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in - if is_empty_type sigma ccl then + if is_empty_type env sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) diff --git a/tactics/elim.ml b/tactics/elim.ml index 003b069b6e61..71ea0098a322 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -81,12 +81,13 @@ let up_to_delta = ref false (* true *) let general_decompose recognizer c = Proofview.Goal.enter begin fun gl -> let type_of = pf_unsafe_type_of gl in + let env = pf_env gl in let sigma = project gl in let typc = type_of c in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId - (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma)) + (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma)) (fun id -> clear [id]))); exact_no_check c ] end @@ -105,17 +106,17 @@ let head_in indl t gl = let decompose_these c l = Proofview.Goal.enter begin fun gl -> let indl = List.map (fun x -> x, Univ.Instance.empty) l in - general_decompose (fun sigma (_,t) -> head_in indl t gl) c + general_decompose (fun env sigma (_,t) -> head_in indl t gl) c end let decompose_and c = general_decompose - (fun sigma (_,t) -> is_record sigma t) + (fun env sigma (_,t) -> is_record env sigma t) c let decompose_or c = general_decompose - (fun sigma (_,t) -> is_disjunction sigma t) + (fun env sigma (_,t) -> is_disjunction env sigma t) c let h_decompose l c = decompose_these c l diff --git a/tactics/equality.ml b/tactics/equality.ml index d5fdad012734..3d760f1c3dbf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -446,7 +446,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in - match match_with_equality_type sigma t with + match match_with_equality_type env sigma t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) @@ -462,7 +462,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *) - match match_with_equality_type sigma t' with + match match_with_equality_type env sigma t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c @@ -743,7 +743,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = let hd2,args2 = whd_all_stack env sigma t2 in match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_) - when Int.equal (List.length args1) (constructor_nallargs_env env sp1) + when Int.equal (List.length args1) (constructor_nallargs env sp1) -> let sorts' = Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) @@ -751,7 +751,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 = (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) if eq_constructor sp1 sp2 then - let nparams = inductive_nparams_env env ind1 in + let nparams = inductive_nparams env ind1 in let params1,rargs1 = List.chop nparams args1 in let _,rargs2 = List.chop nparams args2 in let (mib,mip) = lookup_mind_specif env ind1 in @@ -966,9 +966,10 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> + let env = pf_env gl in let sigma = project gl in let hyp_typ = pf_get_hyp_typ id gl in - if is_empty_type sigma hyp_typ + if is_empty_type env sigma hyp_typ then simplest_elim (mkVar id) else @@ -1066,7 +1067,7 @@ let onNegatedEquality with_evars tac = let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match EConstr.kind sigma (hnf_constr env sigma ccl) with - | Prod (_,t,u) when is_empty_type sigma u -> + | Prod (_,t,u) when is_empty_type env sigma u -> tclTHEN introf (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) diff --git a/tactics/hints.ml b/tactics/hints.ml index 3854606afa06..11a8816159bb 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1355,7 +1355,7 @@ let interp_hints poly = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; - List.init (nconstructors ind) + List.init (nconstructors env ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in empty_hint_info, @@ -1391,7 +1391,7 @@ let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> match EConstr.kind sigma lem with | Ind (ind,u) -> - List.init (nconstructors ind) + List.init (nconstructors env ind) (fun i -> let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd) (Evd.universe_context_set sigma) in diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 08131f6309cd..e1dad9ad209b 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -34,44 +34,42 @@ module RelDecl = Context.Rel.Declaration -- Eduardo (6/8/97). *) -type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option +type 'a matching_function = Environ.env -> Evd.evar_map -> EConstr.constr -> 'a option -type testing_function = Evd.evar_map -> EConstr.constr -> bool +type testing_function = Environ.env -> Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let op2bool = function Some _ -> true | None -> false - -let match_with_non_recursive_type sigma t = +let match_with_non_recursive_type env sigma t = match EConstr.kind sigma t with | App _ -> let (hdapp,args) = decompose_app sigma t in (match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then + if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then Some (hdapp,args) else None | _ -> None) | _ -> None -let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t) +let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursive_type env sigma t) (* Test dependencies *) (* NB: we consider also the let-in case in the following function, since they may appear in types of inductive constructors (see #2629) *) -let rec has_nodep_prod_after n sigma c = +let rec has_nodep_prod_after n env sigma c = match EConstr.kind sigma c with | Prod (_,_,b) | LetIn (_,_,_,b) -> ( n>0 || Vars.noccurn sigma 1 b) - && (has_nodep_prod_after (n-1) sigma b) + && (has_nodep_prod_after (n-1) env sigma b) | _ -> true -let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c +let has_nodep_prod env sigma c = has_nodep_prod_after 0 env sigma c (* A general conjunctive type is a non-recursive with-no-indices inductive type with only one constructor and no dependencies between argument; @@ -96,11 +94,11 @@ let rec whd_beta_prod sigma c = match EConstr.kind sigma c with | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c) | _ -> c -let match_with_one_constructor sigma style onlybinary allow_rec t = +let match_with_one_constructor env sigma style onlybinary allow_rec t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with | Ind ind -> - let (mib,mip) = Global.lookup_inductive (fst ind) in + let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in if Int.equal (Array.length mip.mind_consnames) 1 && (allow_rec || not (mis_is_recursive (fst ind,mib,mip))) && (Int.equal mip.mind_nrealargs 0) @@ -125,7 +123,7 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = let ctyp = whd_beta_prod sigma (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in - if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then + if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) else @@ -138,20 +136,20 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = | Some (hdapp, [_; _]) -> res | _ -> None -let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t = - match_with_one_constructor sigma (Some strict) onlybinary false t +let match_with_conjunction ?(strict=false) ?(onlybinary=false) env sigma t = + match_with_one_constructor env sigma (Some strict) onlybinary false t -let match_with_record sigma t = - match_with_one_constructor sigma None false false t +let match_with_record env sigma t = + match_with_one_constructor env sigma None false false t -let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t = - op2bool (match_with_conjunction sigma ~strict ~onlybinary t) +let is_conjunction ?(strict=false) ?(onlybinary=false) env sigma t = + Option.has_some (match_with_conjunction env sigma ~strict ~onlybinary t) -let is_record sigma t = - op2bool (match_with_record sigma t) +let is_record env sigma t = + Option.has_some (match_with_record env sigma t) -let match_with_tuple sigma t = - let t = match_with_one_constructor sigma None false true t in +let match_with_tuple env sigma t = + let t = match_with_one_constructor env sigma None false true t in Option.map (fun (hd,l) -> let ind = destInd sigma hd in let ind = on_snd (fun u -> EInstance.kind sigma u) ind in @@ -159,8 +157,8 @@ let match_with_tuple sigma t = let isrec = mis_is_recursive (fst ind,mib,mip) in (hd,l,isrec)) t -let is_tuple sigma t = - op2bool (match_with_tuple sigma t) +let is_tuple env sigma t = + Option.has_some (match_with_tuple env sigma t) (* A general disjunction type is a non-recursive with-no-indices inductive type with of which all constructors have a single argument; @@ -175,11 +173,11 @@ let test_strict_disjunction (mib, mip) = in Array.for_all_i check 0 mip.mind_nf_lc -let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = +let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = let (hdapp,args) = decompose_app sigma t in let res = match EConstr.kind sigma hdapp with | Ind (ind,u) -> - let car = constructors_nrealargs ind in + let car = constructors_nrealargs env ind in let (mib,mip) = Global.lookup_inductive ind in if Array.for_all (fun ar -> Int.equal ar 1) car && not (mis_is_recursive (ind,mib,mip)) @@ -205,31 +203,31 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = | Some (hdapp,[_; _]) -> res | _ -> None -let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t = - op2bool (match_with_disjunction ~strict ~onlybinary sigma t) +let is_disjunction ?(strict=false) ?(onlybinary=false) env sigma t = + Option.has_some (match_with_disjunction ~strict ~onlybinary env sigma t) (* An empty type is an inductive type, possible with indices, that has no constructors *) -let match_with_empty_type sigma t = +let match_with_empty_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 0 then Some hdapp else None | _ -> None -let is_empty_type sigma t = op2bool (match_with_empty_type sigma t) +let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t) (* This filters inductive types with one constructor with no arguments; Parameters and indices are allowed *) -let match_with_unit_or_eq_type sigma t = +let match_with_unit_or_eq_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind , _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then Some hdapp @@ -237,14 +235,14 @@ let match_with_unit_or_eq_type sigma t = None | _ -> None -let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t) +let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t) (* A unit type is an inductive type with no indices but possibly (useless) parameters, and that has no arguments in its unique constructor *) -let is_unit_type sigma t = - match match_with_conjunction sigma t with +let is_unit_type env sigma t = + match match_with_conjunction env sigma t with | Some (_,[]) -> true | _ -> false @@ -331,15 +329,16 @@ let match_with_equation env sigma t = let is_inductive_equality ind = let (mib,mip) = Global.lookup_inductive ind in let nconstr = Array.length mip.mind_consnames in - Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0 + let env = Global.env () in + Int.equal nconstr 1 && Int.equal (constructor_nrealargs env (ind,1)) 0 -let match_with_equality_type sigma t = +let match_with_equality_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args) | _ -> None -let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) +let is_equality_type env sigma t = Option.has_some (match_with_equality_type env sigma t) (* Arrows/Implication/Negation *) @@ -353,39 +352,39 @@ let match_arrow_pattern env sigma t = assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) | _ -> anomaly (Pp.str "Incorrect pattern matching.") -let match_with_imp_term sigma c = +let match_with_imp_term env sigma c = match EConstr.kind sigma c with | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b) | _ -> None -let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) +let is_imp_term env sigma c = Option.has_some (match_with_imp_term env sigma c) let match_with_nottype env sigma t = try let (arg,mind) = match_arrow_pattern env sigma t in - if is_empty_type sigma mind then Some (mind,arg) else None + if is_empty_type env sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None -let is_nottype env sigma t = op2bool (match_with_nottype env sigma t) +let is_nottype env sigma t = Option.has_some (match_with_nottype env sigma t) (* Forall *) -let match_with_forall_term sigma c= +let match_with_forall_term env sigma c = match EConstr.kind sigma c with | Prod (nam,a,b) -> Some (nam,a,b) | _ -> None -let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) +let is_forall_term env sigma c = Option.has_some (match_with_forall_term env sigma c) -let match_with_nodep_ind sigma t = +let match_with_nodep_ind env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> - let (mib,mip) = Global.lookup_inductive ind in + let (mib,mip) = Inductive.lookup_mind_specif env ind in if Array.length (mib.mind_packets)>1 then None else let nodep_constr (ctx, cty) = let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in - has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in + has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) env sigma c in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -395,9 +394,9 @@ let match_with_nodep_ind sigma t = None | _ -> None -let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) +let is_nodep_ind env sigma t = Option.has_some (match_with_nodep_ind env sigma t) -let match_with_sigma_type sigma t = +let match_with_sigma_type env sigma t = let (hdapp,args) = decompose_app sigma t in match EConstr.kind sigma hdapp with | Ind (ind, _) -> @@ -405,7 +404,7 @@ let match_with_sigma_type sigma t = if Int.equal (Array.length (mib.mind_packets)) 1 && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) - && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma + && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) env sigma (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx)) then (*allowing only 1 existential*) @@ -414,7 +413,7 @@ let match_with_sigma_type sigma t = None | _ -> None -let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t) +let is_sigma_type env sigma t = Option.has_some (match_with_sigma_type env sigma t) (***** Destructing patterns bound to some theory *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 741f6713e385..b8c3ddb0f0ac 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -43,8 +43,8 @@ open Coqlib also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97). *) -type 'a matching_function = evar_map -> constr -> 'a option -type testing_function = evar_map -> constr -> bool +type 'a matching_function = Environ.env -> evar_map -> constr -> 'a option +type testing_function = Environ.env -> evar_map -> constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function @@ -83,8 +83,8 @@ val is_inductive_equality : inductive -> bool val match_with_equality_type : (constr * constr list) matching_function val is_equality_type : testing_function -val match_with_nottype : Environ.env -> (constr * constr) matching_function -val is_nottype : Environ.env -> testing_function +val match_with_nottype : (constr * constr) matching_function +val is_nottype : testing_function val match_with_forall_term : (Name.t Context.binder_annot * constr * constr) matching_function val is_forall_term : testing_function diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 53a74a5f7de8..066b9c779468 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1432,7 +1432,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (general_elim with_evars clear_flag (c,lbindc) {elimindex = None; elimbody = (elim,NoBindings); - elimrename = Some (false, constructors_nrealdecls (fst mind))}) + elimrename = Some (false, constructors_nrealdecls env (fst mind))}) end let general_case_analysis with_evars clear_flag (c,lbindc as cx) = @@ -1464,7 +1464,7 @@ let find_eliminator c gl = if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); - elimrename = Some (true, constructors_nrealdecls ind)} + elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)} let default_elim with_evars clear_flag (c,_ as cx) = Proofview.tclORELSE @@ -1610,9 +1610,9 @@ let descend_in_conjunctions avoid tac (err, info) c = let t = Retyping.get_type_of env sigma c in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = EConstr.decompose_prod_assum sigma t in - match match_with_tuple sigma ccl with + match match_with_tuple env sigma ccl with | Some (_,_,isrec) -> - let n = (constructors_nrealargs ind).(0) in + let n = (constructors_nrealargs env ind).(0) in let sort = Tacticals.New.elimination_sort_of_goal gl in let IndType (indf,_) = find_rectype env sigma ccl in let (_,inst), params = dest_ind_family indf in @@ -2300,7 +2300,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in let t = whd_all (type_of (mkVar id)) in - let eqtac, thin = match match_with_equality_type sigma t with + let eqtac, thin = match match_with_equality_type env sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then let id' = destVar sigma lhs in @@ -4740,9 +4740,10 @@ let reflexivity_red allowred = (* PL: usual reflexivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match match_with_equality_type sigma concl with + match match_with_equality_type env sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings end diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 1e733acc5996..642695bda480 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -313,7 +313,9 @@ let warn_cannot_build_congruence = strbrk "Cannot build congruence scheme because eq is not found") let declare_congr_scheme ind = - if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin + let env = Global.env () in + let sigma = Evd.from_env env in + if Hipattern.is_equality_type env sigma (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true with e when CErrors.noncritical e -> false