diff options
66 files changed, 270 insertions, 368 deletions
diff --git a/Makefile.ci b/Makefile.ci index f14203fa4a..c2a3cd7e14 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -45,6 +45,7 @@ CI_TARGETS= \ ci-stdlib2 \ ci-tlc \ ci-unimath \ + ci-unicoq \ ci-verdi-raft \ ci-vst @@ -64,6 +65,8 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-mtac2: ci-unicoq + ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 051f51bbb3..62e732ce69 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -170,7 +170,6 @@ let check_inductive env mind mb = check_guarded = mb_flags.check_guarded; check_positive = mb_flags.check_positive; check_universes = mb_flags.check_universes; - check_template = mb_flags.check_template; conv_oracle = mb_flags.conv_oracle; } env diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d115744707..8854a23dd5 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -56,10 +56,6 @@ let pr_nonpositive env = let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_positive then MutInd.to_string c :: acc else acc) env [] in pr_assumptions "Inductives whose positivity is assumed" inds -let pr_unsafe_template env = - let inds = fold_inductives (fun c cb acc -> if not cb.mind_typing_flags.check_template then MutInd.to_string c :: acc else acc) env [] in - pr_assumptions "Inductives using unchecked template polymorphism" inds - let print_context env = if !output_context then begin Feedback.msg_notice @@ -70,8 +66,8 @@ let print_context env = str "* " ++ hov 0 (pr_axioms env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_type_in_type env ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_unguarded env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_nonpositive env ++ fnl()) ++ fnl() ++ - str "* " ++ hov 0 (pr_unsafe_template env))) + str "* " ++ hov 0 (pr_nonpositive env ++ fnl())) + ) end let stats env = diff --git a/checker/values.ml b/checker/values.ml index c8bbc092b4..ed730cff8e 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -238,7 +238,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_opaque|]; [|v_primitive|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|] let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] diff --git a/default.nix b/default.nix index 174e199014..ae6a8d06e5 100644 --- a/default.nix +++ b/default.nix @@ -77,7 +77,7 @@ stdenv.mkDerivation rec { !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci" "nix"]) ./.; preConfigure = '' - patchShebangs dev/tools/ + patchShebangs dev/tools/ doc/stdlib ''; prefixKey = "-prefix "; diff --git a/dev/ci/ci-mtac2.sh b/dev/ci/ci-mtac2.sh index 7075d4d7f6..e08dcf07ab 100755 --- a/dev/ci/ci-mtac2.sh +++ b/dev/ci/ci-mtac2.sh @@ -3,10 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download unicoq - -( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) - git_download mtac2 ( cd "${CI_BUILD_DIR}/mtac2" && coq_makefile -f _CoqProject -o Makefile && make ) diff --git a/dev/ci/ci-unicoq.sh b/dev/ci/ci-unicoq.sh new file mode 100755 index 0000000000..36acb115e9 --- /dev/null +++ b/dev/ci/ci-unicoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download unicoq + +( cd "${CI_BUILD_DIR}/unicoq" && coq_makefile -f Make -o Makefile && make && make install ) diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 150dad16c2..e37a58be61 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -119,6 +119,20 @@ let isVarId sigma id c = let isRelN sigma n c = match kind sigma c with Rel n' -> Int.equal n n' | _ -> false +let isRef sigma c = match kind sigma c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +let isRefX sigma x c = + let open GlobRef in + match x, kind sigma c with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + + let destRel sigma c = match kind sigma c with | Rel p -> p | _ -> raise DestKO @@ -723,8 +737,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, t -let is_global sigma gr c = - Globnames.is_global gr (to_constr sigma c) +let is_global = isRefX module Unsafe = struct diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 90f50b764c..181714460d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -152,6 +152,7 @@ val mkNamedProd_or_LetIn : named_declaration -> types -> types val isRel : Evd.evar_map -> t -> bool val isVar : Evd.evar_map -> t -> bool val isInd : Evd.evar_map -> t -> bool +val isRef : Evd.evar_map -> t -> bool val isEvar : Evd.evar_map -> t -> bool val isMeta : Evd.evar_map -> t -> bool val isSort : Evd.evar_map -> t -> bool @@ -175,6 +176,7 @@ val isArity : Evd.evar_map -> t -> bool val isVarId : Evd.evar_map -> Id.t -> t -> bool val isRelN : Evd.evar_map -> int -> t -> bool +val isRefX : Evd.evar_map -> GlobRef.t -> t -> bool val destRel : Evd.evar_map -> t -> int val destMeta : Evd.evar_map -> t -> metavariable @@ -319,6 +321,7 @@ val fresh_global : Evd.evar_map -> GlobRef.t -> Evd.evar_map * t val is_global : Evd.evar_map -> GlobRef.t -> t -> bool +[@@ocaml.deprecated "Use [EConstr.isRefX] instead."] (** {5 Extra} *) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b09cc87f97..8533e05d3e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -555,7 +555,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = let () = if global then let check id' = if Id.Set.mem id' ids then - raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) + raise (ClearDependencyError (id',err,Some (fst @@ destRef c))) in Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c)) in diff --git a/engine/termops.ml b/engine/termops.ml index a65b8275e6..a5c179bf78 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1066,19 +1066,9 @@ let global_of_constr sigma c = | Var id -> VarRef id, EConstr.EInstance.empty | _ -> raise Not_found -let is_global sigma c t = - let open GlobRef in - match c, EConstr.kind sigma t with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> Id.equal id id' - | _ -> false +let is_global = EConstr.isRefX -let isGlobalRef sigma c = - match EConstr.kind sigma c with - | Const _ | Ind _ | Construct _ | Var _ -> true - | _ -> false +let isGlobalRef = EConstr.isRef let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with diff --git a/engine/termops.mli b/engine/termops.mli index f970b9ece0..7bbf87239d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -264,10 +264,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. val is_section_variable : Id.t -> bool val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t +[@@ocaml.deprecated "Use [EConstr.destRef] instead (throws DestKO instead of Not_found)."] val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool +[@@ocaml.deprecated "Use [EConstr.isRefX] instead."] val isGlobalRef : Evd.evar_map -> constr -> bool +[@@ocaml.deprecated "Use [EConstr.isRef] instead."] val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool diff --git a/interp/reserve.ml b/interp/reserve.ml index e81439c3d5..4a731e57a3 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -104,8 +104,8 @@ let declare_reserved_type idl t = let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table let constr_key c = - try RefKey (canonical_gr (global_of_constr (fst (Constr.decompose_app c)))) - with Not_found -> Oth + try RefKey (canonical_gr (fst @@ Constr.destRef (fst (Constr.decompose_app c)))) + with Constr.DestKO -> Oth let revert_reserved_type t = try diff --git a/kernel/constr.ml b/kernel/constr.ml index 15e5c512ed..84eacb196c 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -253,7 +253,7 @@ let mkFloat f = Float f least one argument and the function is not itself an applicative term *) -let kind c = c +let kind (c:t) = c let rec kind_nocast_gen kind c = match kind c with @@ -338,6 +338,19 @@ let isProj c = match kind c with Proj _ -> true | _ -> false let isFix c = match kind c with Fix _ -> true | _ -> false let isCoFix c = match kind c with CoFix _ -> true | _ -> false +let isRef c = match kind c with + | Const _ | Ind _ | Construct _ | Var _ -> true + | _ -> false + +let isRefX x c = + let open GlobRef in + match x, kind c with + | ConstRef c, Const (c', _) -> Constant.equal c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> Id.equal id id' + | _ -> false + (* Destructs a de Bruijn index *) let destRel c = match kind c with | Rel n -> n diff --git a/kernel/constr.mli b/kernel/constr.mli index d4af1149c2..159570b5ea 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -256,6 +256,8 @@ val isRel : constr -> bool val isRelN : int -> constr -> bool val isVar : constr -> bool val isVarId : Id.t -> constr -> bool +val isRef : constr -> bool +val isRefX : GlobRef.t -> constr -> bool val isInd : constr -> bool val isEvar : constr -> bool val isMeta : constr -> bool diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f1eb000c88..31dd26d2ba 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -258,17 +258,6 @@ let cook_constant { from = cb; info } = (********************************) (* Discharging mutual inductive *) -let template_level_of_var ~template_check d = - (* When [template_check], a universe from a section variable may not - be in the universes from the inductive (it must be pre-declared) - so always [None]. *) - if template_check then None - else - let c = Term.strip_prod_assum (RelDecl.get_type d) in - match kind c with - | Sort (Type u) -> Univ.Universe.level u - | _ -> None - let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c) let abstract_rel_ctx (section_decls,subst) ctx = @@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t = let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in t -let cook_one_ind ~template_check ~ntypes +let cook_one_ind ~ntypes (section_decls,_ as hyps) expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> @@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes RegularArity {mind_user_arity=arity; mind_sort=sort} | TemplateArity {template_param_levels=levels;template_level;template_context} -> let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d) + if RelDecl.is_local_assum d then Some None else None) section_decls in @@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = let removed_vars = Context.Named.to_vars section_decls in let section_decls, _ as hyps = abstract_context section_decls in let nnewparams = Context.Rel.nhyps section_decls in - let template_check = mib.mind_typing_flags.check_template in let mind_params_ctxt = let ctx = Context.Rel.map expmod mib.mind_params_ctxt in abstract_rel_ctx hyps ctx in let ntypes = mib.mind_ntypes in let mind_packets = - Array.map (cook_one_ind ~template_check ~ntypes hyps expmod) + Array.map (cook_one_ind ~ntypes hyps expmod) mib.mind_packets in let mind_record = match mib.mind_record with diff --git a/kernel/declarations.ml b/kernel/declarations.ml index c550b0d432..ac130d018d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -89,10 +89,6 @@ type typing_flags = { indices_matter: bool; (** The universe of an inductive type must be above that of its indices. *) - check_template : bool; - (* If [false] then we don't check that the universes template-polymorphic - inductive parameterize on are necessarily local and unbounded from below. - This potentially introduces inconsistencies. *) } (* some contraints are in constant_constraints, some other may be in diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 047027984d..a3adac7a11 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -26,7 +26,6 @@ let safe_flags oracle = { enable_VM = true; enable_native_compiler = true; indices_matter = true; - check_template = true; } (** {6 Arities } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index f04863386f..501ac99ff3 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let indices_matter env = env.env_typing_flags.indices_matter -let check_template env = env.env_typing_flags.check_template let universes env = env.env_stratification.env_universes let universes_lbound env = env.env_stratification.env_universes_lbound @@ -399,9 +398,6 @@ let add_constraints c env = let check_constraints c env = UGraph.check_constraints c env.env_stratification.env_universes -let push_constraints_to_env (_,univs) env = - add_constraints univs env - let add_universes ~lbound ~strict ctx g = let g = Array.fold_left (fun g v -> UGraph.add_universe ~lbound ~strict v g) @@ -449,7 +445,6 @@ let same_flags { share_reduction; enable_VM; enable_native_compiler; - check_template; } alt = check_guarded == alt.check_guarded && check_positive == alt.check_positive && @@ -458,8 +453,7 @@ let same_flags { indices_matter == alt.indices_matter && share_reduction == alt.share_reduction && enable_VM == alt.enable_VM && - enable_native_compiler == alt.enable_native_compiler && - check_template == alt.check_template + enable_native_compiler == alt.enable_native_compiler [@warning "+9"] let set_typing_flags c env = (* Unsafe *) @@ -591,9 +585,6 @@ let polymorphic_pind (ind,u) env = let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes -let template_checked_ind (mind,_i) env = - (lookup_mind mind env).mind_typing_flags.check_template - let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with | TemplateArity _ -> true @@ -802,14 +793,6 @@ let get_template_polymorphic_variables env r = | IndRef ind -> template_polymorphic_variables ind env | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env -let is_template_checked env r = - let open Names.GlobRef in - match r with - | VarRef _id -> false - | ConstRef _c -> false - | IndRef ind -> template_checked_ind ind env - | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env - let is_type_in_type env r = let open Names.GlobRef in match r with diff --git a/kernel/environ.mli b/kernel/environ.mli index bd5a000c2b..a596584cbe 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool val type_in_type : env -> bool val deactivated_guard : env -> bool val indices_matter : env -> bool -val check_template : env -> bool val is_impredicative_sort : env -> Sorts.t -> bool val is_impredicative_univ : env -> Univ.Universe.t -> bool @@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool val template_polymorphic_ind : inductive -> env -> bool val template_polymorphic_variables : inductive -> env -> Univ.Level.t list val template_polymorphic_pind : pinductive -> env -> bool -val template_checked_ind : inductive -> env -> bool (** {5 Modules } *) @@ -288,22 +286,21 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) -(** Add universe constraints to the environment. - @raise UniverseInconsistency . -*) val add_constraints : Univ.Constraint.t -> env -> env +(** Add universe constraints to the environment. + @raise UniverseInconsistency. *) -(** Check constraints are satifiable in the environment. *) val check_constraints : Univ.Constraint.t -> env -> bool +(** Check constraints are satifiable in the environment. *) + val push_context : ?strict:bool -> Univ.UContext.t -> env -> env -(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment. - @raise UGraph.AlreadyDeclared if one of the universes is already declared. -*) -val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env -(* [push_context_set ?(strict=false) ctx env] pushes the universe context set - to the environment. It does not fail if one of the universes is already declared. *) +(** [push_context ?(strict=false) ctx env] pushes the universe context to the environment. + @raise UGraph.AlreadyDeclared if one of the universes is already declared. *) -val push_constraints_to_env : 'a Univ.constrained -> env -> env +val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env +(** [push_context_set ?(strict=false) ctx env] pushes the universe + context set to the environment. It does not fail even if one of the + universes is already declared. *) val push_subgraph : Univ.ContextSet.t -> env -> env (** [push_subgraph univs env] adds the universes and constraints in @@ -373,7 +370,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list -val is_template_checked : env -> GlobRef.t -> bool val is_type_in_type : env -> GlobRef.t -> bool (** Native compiler *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 113ee787f2..cc15109f06 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -197,7 +197,7 @@ let unbounded_from_below u cstrs = (starting from the most recent and ignoring let-definitions) is not contributing to the inductive type's sort or is Some u_k if its level is u_k and is contributing. *) -let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl = +let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && @@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc in let univs = Univ.Universe.levels concl in let univs = - if template_check then - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - else univs (* Doesn't check the universes can be generalized *) + Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> - if template_check then (match Univ.Universe.level u with | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None | None -> None) - else Univ.Universe.level u | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in params, univs -let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp splayed_lc in let param_levels, concl_levels = - template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ + template_polymorphic_univs ~ctor_levels ctx params min_univ in - if template_check && List.for_all (fun x -> Option.is_empty x) param_levels + if List.for_all (fun x -> Option.is_empty x) param_levels && Univ.LSet.is_empty concl_levels then CErrors.user_err Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") @@ -356,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let template_check = Environ.check_template env in - let data = List.map (abstract_packets ~template_check univs usubst params) data in + let data = List.map (abstract_packets univs usubst params) data in let env_ar_par = let ctx = Environ.rel_context env_ar_par in diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 8dea8f046d..723ba5459e 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option (* Utility function to compute the actual universe parameters of a template polymorphic inductive *) val template_polymorphic_univs : - template_check:bool -> ctor_levels:Univ.LSet.t -> Univ.ContextSet.t -> Constr.rel_context -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ca4fea45c5..5d8e1f0fdb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -198,7 +198,14 @@ let relevance_of_inductive env ind = let _, mip = lookup_mind_specif env ind in mip.mind_relevance -let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = +let check_instance mib u = + if not (match mib.mind_universes with + | Monomorphic _ -> Instance.is_empty u + | Polymorphic uctx -> Instance.length u = AUContext.size uctx) + then CErrors.anomaly Pp.(str "bad instance length on mutind.") + +let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = + check_instance mib u; match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -244,6 +251,7 @@ let max_inductive_sort = (* Type of a constructor *) let type_of_constructor (cstr, u) (mib,mip) = + check_instance mib u; let ind = inductive_of_constructor cstr in let specif = mip.mind_user_lc in let i = index_of_constructor cstr in diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index c2cdf98ee8..6c06c1e0f1 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -48,7 +48,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -182,7 +182,7 @@ let map_ptype_error f = function | UnboundVar id -> UnboundVar id | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) -| ReferenceVariables (id, c) -> ReferenceVariables (id, f c) +| ReferenceVariables (id, c) -> ReferenceVariables (id, c) | ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 0f29717f12..d9842ecefa 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -102,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a val error_assumption : env -> unsafe_judgment -> 'a -val error_reference_variables : env -> Id.t -> constr -> 'a +val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a val error_elim_arity : env -> pinductive -> constr -> unsafe_judgment -> diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c74bfd0688..2a35f87db8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -116,7 +116,7 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env ?evars f c sign = +let check_hyps_inclusion env ?evars c sign = let conv env a b = conv env ?evars a b in Context.Named.fold_outside (fun d1 () -> @@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id (f c)) + error_reference_variables env id c) sign ~init:() @@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign = let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -368,18 +368,18 @@ let check_cast env c ct k expected_type = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let type_of_inductive_knowing_parameters env (ind,u as indu) args = +let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in check_constraints cst env; t -let type_of_inductive env (ind,u as indu) = +let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in check_constraints cst env; t @@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps + check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index ae816fe26e..f88bc653de 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> - ('a -> constr) -> 'a -> Constr.named_context -> unit + GlobRef.t -> Constr.named_context -> unit val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit diff --git a/library/global.ml b/library/global.ml index fbbe09301b..8706238f5a 100644 --- a/library/global.ml +++ b/library/global.ml @@ -192,8 +192,6 @@ let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r -let is_template_checked r = is_template_checked (env ()) r - let get_template_polymorphic_variables r = get_template_polymorphic_variables (env ()) r let is_type_in_type r = is_type_in_type (env ()) r diff --git a/library/global.mli b/library/global.mli index b6bd69c17c..0198ac5952 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,7 +150,6 @@ val is_joined_environment : unit -> bool val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool -val is_template_checked : GlobRef.t -> bool val get_template_polymorphic_variables : GlobRef.t -> Univ.Level.t list val is_type_in_type : GlobRef.t -> bool diff --git a/library/globnames.ml b/library/globnames.ml index 63cb2c69bd..e55a7b5499 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -73,13 +73,7 @@ let global_of_constr c = match kind c with | Var id -> VarRef id | _ -> raise Not_found -let is_global c t = - match c, kind t with - | ConstRef c, Const (c', _) -> Constant.equal c c' - | IndRef i, Ind (i', _) -> eq_ind i i' - | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> Id.equal id id' - | _ -> false +let is_global = Constr.isRefX let printable_constr_of_global = function | VarRef id -> mkVar id diff --git a/library/globnames.mli b/library/globnames.mli index d61cdd2b64..fb59cbea4e 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -32,6 +32,7 @@ val destIndRef : GlobRef.t -> inductive val destConstructRef : GlobRef.t -> constructor val is_global : GlobRef.t -> constr -> bool +[@@ocaml.deprecated "Use [Constr.isRefX] instead."] val subst_constructor : substitution -> constructor -> constructor val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option @@ -44,6 +45,7 @@ val printable_constr_of_global : GlobRef.t -> constr (** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t +[@@ocaml.deprecated "Use [Constr.destRef] instead (throws DestKO instead of Not_found)."] (** {6 Extended global references } *) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8a650d9e7a..9ea2224272 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -90,14 +90,13 @@ let rec decompose_term env sigma t= if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found (* decompose equality in members and type *) -open Termops let atom_of_constr env sigma term = let wh = whd_delta env sigma term in let kot = EConstr.kind sigma wh in match kot with App (f,args)-> - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then `Eq (args.(0), decompose_term env sigma args.(1), decompose_term env sigma args.(2)) @@ -132,7 +131,7 @@ let non_trivial = function let patterns_of_constr env sigma nrels term= let f,args= try destApp sigma (whd_delta env sigma term) with DestKO -> raise Not_found in - if is_global sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 + if isRefX sigma (Lazy.force _eq) f && Int.equal (Array.length args) 3 then let patt1,rels1 = pattern_of_constr env sigma args.(1) and patt2,rels2 = pattern_of_constr env sigma args.(2) in @@ -153,7 +152,7 @@ let patterns_of_constr env sigma nrels term= let rec quantified_atom_of_constr env sigma nrels term = match EConstr.kind sigma (whd_delta env sigma term) with Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else @@ -165,7 +164,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let litteral_of_constr env sigma term= match EConstr.kind sigma (whd_delta env sigma term) with | Prod (id,atom,ff) -> - if is_global sigma (Lazy.force _False) ff then + if isRefX sigma (Lazy.force _False) ff then match (atom_of_constr env sigma atom) with `Eq(t,a,b) -> `Neq(t,a,b) | `Other(p) -> `Nother(p) @@ -517,7 +516,7 @@ let f_equal = in Proofview.tclORELSE begin match EConstr.kind sigma concl with - | App (r,[|_;t;t'|]) when is_global sigma (Lazy.force _eq) r -> + | App (r,[|_;t;t'|]) when isRefX sigma (Lazy.force _eq) r -> begin match EConstr.kind sigma t, EConstr.kind sigma t' with | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') -> let rec cuts i = diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 65af123d9c..c77ddeb040 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -209,11 +209,11 @@ let extend_with_auto_hints env sigma l seq = | Res_pf (c,_) | Give_exact (c,_) | Res_pf_THEN_trivial_fail (c,_) -> let (c, _, _) = c in - (try - let (gr, _) = Termops.global_of_constr sigma c in + (match EConstr.destRef sigma c with + | exception Constr.DestKO -> seq, sigma + | gr, _ -> let sigma, typ = Typing.type_of env sigma c in - add_formula env sigma Hint gr typ seq, sigma - with Not_found -> seq, sigma) + add_formula env sigma Hint gr typ seq, sigma) | _ -> seq, sigma in let h acc dbname = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index a0eefd1a39..fbc64d95d0 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -289,18 +289,18 @@ end) = struct if Int.equal n 0 then c else match EConstr.kind sigma c with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> decomp_pointwise sigma (pred n) relb - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> decomp_pointwise sigma (pred n) (Reductionops.beta_applist sigma (arelb, [mkRel 1])) | _ -> invalid_arg "decomp_pointwise" let rec apply_pointwise sigma rel = function | arg :: args -> (match EConstr.kind sigma rel with - | App (f, [| a; b; relb |]) when Termops.is_global sigma (pointwise_relation_ref ()) f -> + | App (f, [| a; b; relb |]) when isRefX sigma (pointwise_relation_ref ()) f -> apply_pointwise sigma relb args - | App (f, [| a; b; arelb |]) when Termops.is_global sigma (forall_relation_ref ()) f -> + | App (f, [| a; b; arelb |]) when isRefX sigma (forall_relation_ref ()) f -> apply_pointwise sigma (Reductionops.beta_applist sigma (arelb, [arg])) args | _ -> invalid_arg "apply_pointwise") | [] -> rel @@ -357,7 +357,7 @@ end) = struct match EConstr.kind sigma t with | App (c, args) when Array.length args >= 2 -> let head = if isApp sigma c then fst (destApp sigma c) else c in - if Termops.is_global sigma (coq_eq_ref ()) head then None + if isRefX sigma (coq_eq_ref ()) head then None else (try let params, args = Array.chop (Array.length args - 2) args in @@ -1880,13 +1880,13 @@ let declare_projection n instance_id r = let rec aux t = match EConstr.kind sigma t with | App (f, [| a ; a' ; rel; rel' |]) - when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + when isRefX sigma (PropGlobal.respectful_ref ()) f -> succ (aux rel') | _ -> 0 in let init = match EConstr.kind sigma typ with - App (f, args) when Termops.is_global sigma (PropGlobal.respectful_ref ()) f -> + App (f, args) when isRefX sigma (PropGlobal.respectful_ref ()) f -> mkApp (f, fst (Array.chop (Array.length args - 2) args)) | _ -> typ in aux init diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index a57cc76faa..de70fb292a 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -341,8 +341,8 @@ let coerce_to_reference sigma v = match Value.to_constr v with | Some c -> begin - try fst (Termops.global_of_constr sigma c) - with Not_found -> raise (CannotCoerceTo "a reference") + try fst (EConstr.destRef sigma c) + with DestKO -> raise (CannotCoerceTo "a reference") end | None -> raise (CannotCoerceTo "a reference") diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f7e4a95a22..3841501b6a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -18,7 +18,6 @@ open EConstr open Vars open CClosure open Environ -open Globnames open Glob_term open Locus open Tacexpr @@ -43,12 +42,12 @@ type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_fl let global_head_of_constr sigma c = let f, args = decompose_app sigma c in - try fst (Termops.global_of_constr sigma f) - with Not_found -> CErrors.anomaly (str "global_head_of_constr.") + try fst (EConstr.destRef sigma f) + with DestKO -> CErrors.anomaly (str "global_head_of_constr.") let global_of_constr_nofail c = - try global_of_constr c - with Not_found -> GlobRef.VarRef (Id.of_string "dummy") + try fst @@ Constr.destRef c + with DestKO -> GlobRef.VarRef (Id.of_string "dummy") let rec mk_clos_but f_map n t = let (f, args) = Constr.decompose_appvect t in @@ -97,9 +96,9 @@ let protect_tac_in map id = let rec closed_under sigma cset t = try - let (gr, _) = Termops.global_of_constr sigma t in + let (gr, _) = destRef sigma t in GlobRef.Set_env.mem gr cset - with Not_found -> + with DestKO -> match EConstr.kind sigma t with | Cast(c,_,_) -> closed_under sigma cset c | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l @@ -758,22 +757,21 @@ let af_ar = my_reference"AF_AR" let f_r = my_reference"F_R" let sf_sr = my_reference"SF_SR" let dest_field env evd th_spec = - let open Termops in let th_typ = Retyping.get_type_of env !evd th_spec in match EConstr.kind !evd th_typ with | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global !evd (Lazy.force afield_theory) f -> + when isRefX !evd (Lazy.force afield_theory) f -> let rth = plapp evd af_ar [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (None,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|]) - when is_global !evd (Lazy.force field_theory) f -> + when isRefX !evd (Lazy.force field_theory) f -> let rth = plapp evd f_r [|r;zero;one;add;mul;sub;opp;div;inv;req;th_spec|] in (Some false,r,zero,one,add,mul,Some sub,Some opp,div,inv,req,rth) | App(f,[|r;zero;one;add;mul;div;inv;req|]) - when is_global !evd (Lazy.force sfield_theory) f -> + when isRefX !evd (Lazy.force sfield_theory) f -> let rth = plapp evd sf_sr [|r;zero;one;add;mul;div;inv;req;th_spec|] in (Some true,r,zero,one,add,mul,None,None,div,inv,req,rth) diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 6cb464918a..915531cf3c 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -34,7 +34,6 @@ open Tacinterp open Pretyping open Ppconstr open Printer -open Globnames open Namegen open Evar_kinds open Constrexpr @@ -464,7 +463,7 @@ let nb_cs_proj_args pc f u = | Sort s -> na (Sort_cs (Sorts.family s)) | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f - | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) + | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 3bd52088c7..c21af82659 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -269,7 +269,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) = let sk2 = Stack.append_app args sk2 in lookup_canonical_conversion (proji, Const_cs c2), sk2 | _ -> - let (c2, _) = Termops.global_of_constr sigma t2 in + let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in lookup_canonical_conversion (proji, Const_cs c2),sk2 with Not_found -> let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 36b405e981..816a8c4703 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -28,14 +28,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 3b918b5396..879c007198 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -189,7 +189,7 @@ let rec cs_pattern_of_constr env t = let _, params = Inductive.find_rectype env ty in Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c] | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> Const_cs (Globnames.global_of_constr t) , None, [] + | _ -> Const_cs (fst @@ destRef t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" @@ -234,7 +234,7 @@ let compute_canonical_projections env ~warn (gref,ind) = ((GlobRef.ConstRef proji_sp, (patt, t)), { o_ORIGIN = gref ; o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) :: acc - | exception Not_found -> + | exception DestKO -> if warn then warn_projection_no_head_constant (sign, env, t, gref, proji_sp); acc ) acc spopt diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index f87c50b5e4..4afed07eda 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1311,11 +1311,9 @@ let reduce_to_ref_gen allow_product env sigma ref t = else error_cannot_recognize ref | _ -> - try - if GlobRef.equal (fst (global_of_constr sigma c)) ref - then it_mkProd_or_LetIn t l - else raise Not_found - with Not_found -> + if isRefX sigma ref c + then it_mkProd_or_LetIn t l + else try let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in elimrec env t' l diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1541e96635..d5c8c3bd19 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -107,9 +107,9 @@ let class_info env sigma c = not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.find gr !classes, u - with Not_found -> not_a_class env sigma c + with DestKO | Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in @@ -125,9 +125,9 @@ let class_of_constr env sigma c = with e when CErrors.noncritical e -> None let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in @@ -140,9 +140,9 @@ let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_maybe_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4582844b71..b4c19775a7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,6 +27,8 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration +module GR = Names.GlobRef + let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -287,37 +289,36 @@ let judge_of_letin env name defj typj j = { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } -let check_hyps_inclusion env sigma f x hyps = +let check_hyps_inclusion env sigma x hyps = let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in - let f x = EConstr.Unsafe.to_constr (f x) in - Typeops.check_hyps_inclusion env ~evars f x hyps + Typeops.check_hyps_inclusion env ~evars x hyps let type_of_constant env sigma (c,u) = let open Declarations in let cb = Environ.lookup_constant c env in - let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in + let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in let u = EInstance.kind sigma u in let ty, csts = Environ.constant_type env (c,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c))) let type_of_inductive env sigma (ind,u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind))) + sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) let type_of_constructor env sigma ((ind,_ as ctor),u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor))) let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2416819a6a..f9f46e1ceb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -224,7 +224,7 @@ let tag_var = tag Tag.variable let pr_opt_type_spc pr = function | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt () - | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t + | t -> str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t let pr_prim_token = function | Numeral (SPlus,n) -> str (NumTok.to_string n) @@ -387,12 +387,12 @@ let tag_var = tag Tag.variable if is_open then pr_delimited_binders pr_com_at sep pr_c else pr_undelimited_binders sep pr_c - let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = + let pr_recursive_decl pr pr_dangling kw dangling_with_for id bl annot t c = let pr_body = if dangling_with_for then pr_dangling else pr in - pr_id id ++ (if bl = [] then mt () else str" ") ++ + hov 0 (str kw ++ brk(1,2) ++ pr_id id ++ (if bl = [] then mt () else brk(1,2)) ++ hov 0 (pr_undelimited_binders spc (pr ltop) bl ++ annot) ++ - pr_opt_type_spc pr t ++ str " :=" ++ + pr_opt_type_spc pr t ++ str " :=") ++ pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c let pr_guard_annot pr_aux bl ro = @@ -407,28 +407,28 @@ let tag_var = tag Tag.variable | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then - spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" + spc() ++ str "{" ++ keyword "struct" ++ brk (1,1) ++ pr_id id ++ str"}" else mt() | CWfRec (id,c) -> - spc() ++ str "{" ++ keyword "wf" ++ spc () ++ pr_aux c ++ spc() ++ pr_lident id ++ str"}" + spc() ++ str "{" ++ keyword "wf" ++ brk (1,1) ++ pr_aux c ++ brk (1,1) ++ pr_lident id ++ str"}" | CMeasureRec (id,m,r) -> - spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ - match id with None -> mt() | Some id -> spc () ++ pr_lident id ++ + spc() ++ str "{" ++ keyword "measure" ++ brk (1,1) ++ pr_aux m ++ + match id with None -> mt() | Some id -> brk (1,1) ++ pr_lident id ++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = + let pr_fixdecl pr prd kw dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in - pr_recursive_decl pr prd dangling_with_for id bl annot t c + pr_recursive_decl pr prd kw dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = - pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c + let pr_cofixdecl pr prd kw dangling_with_for ({v=id},bl,t,c) = + pr_recursive_decl pr prd kw dangling_with_for id bl (mt()) t c - let pr_recursive pr_decl id = function + let pr_recursive kw pr_decl id = function | [] -> anomaly (Pp.str "(co)fixpoint with no definition.") - | [d1] -> pr_decl false d1 + | [d1] -> pr_decl kw false d1 | dl -> - prlist_with_sep (fun () -> fnl() ++ keyword "with" ++ spc ()) - (pr_decl true) dl ++ + prlist_with_sep (fun () -> fnl()) + (pr_decl "with" true) dl ++ fnl() ++ keyword "for" ++ spc () ++ pr_id id let pr_asin pr na indnalopt = @@ -494,15 +494,13 @@ let tag_var = tag Tag.variable return (pr_cref r us, latom) | CFix (id,fix) -> return ( - hov 0 (keyword "fix" ++ spc () ++ - pr_recursive + hv 0 (pr_recursive "fix" (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( - hov 0 (keyword "cofix" ++ spc () ++ - pr_recursive + hv 0 (pr_recursive "cofix" (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) diff --git a/printing/printer.ml b/printing/printer.ml index 97e0528939..8af4d1d932 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -859,8 +859,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = @@ -880,13 +878,10 @@ struct Constant.CanOrd.compare k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 - | TemplatePolymorphic m1, TemplatePolymorphic m2 -> - MutInd.CanOrd.compare m1 m2 | Guarded k1 , Guarded k2 -> GlobRef.Ordered.compare k1 k2 | _ , Constant _ -> 1 | _ , Positive _ -> 1 - | _, TemplatePolymorphic _ -> 1 | _ -> -1 let compare x y = @@ -947,9 +942,6 @@ let pr_assumptionset env sigma s = hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.") - | TemplatePolymorphic m -> - hov 2 (safe_pr_inductive env m ++ spc () ++ - strbrk"is assumed template polymorphic on all its universe parameters.") | TypeInType gr -> hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.") in diff --git a/printing/printer.mli b/printing/printer.mli index 1d7a25cbb6..cd5151bd8f 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -231,8 +231,6 @@ type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *) - | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism - on parameter universes has not been checked. *) | TypeInType of GlobRef.t (* a constant which relies on type in type *) type context_object = diff --git a/tactics/equality.ml b/tactics/equality.ml index 9195746dc6..9ef5f478d3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot = Proofview.Goal.enter_one begin fun gl -> let sigma = project gl in let is_global_exists gr c = - Coqlib.has_ref gr && Termops.is_global sigma (Coqlib.lib_ref gr) c + Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c in let inccl = Option.is_empty cls in let env = Proofview.Goal.env gl in @@ -1339,11 +1339,11 @@ let inject_if_homogenous_dependent_pair ty = let existTconstr = Coqlib.lib_ref "core.sigT.intro" in (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app sigma t) in - if not (Termops.is_global sigma sigTconstr eqTypeDest) then raise Exit; + if not (isRefX sigma sigTconstr eqTypeDest) then raise Exit; let hd1,ar1 = decompose_app_vect sigma t1 and hd2,ar2 = decompose_app_vect sigma t2 in - if not (Termops.is_global sigma existTconstr hd1) then raise Exit; - if not (Termops.is_global sigma existTconstr hd2) then raise Exit; + if not (isRefX sigma existTconstr hd1) then raise Exit; + if not (isRefX sigma existTconstr hd2) then raise Exit; let (ind, _), _ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in (* check if the user has declared the dec principle *) (* and compare the fst arguments of the dep pair *) @@ -1692,8 +1692,8 @@ let () = optwrite = (:=) regular_subst_tactic } let restrict_to_eq_and_identity eq = (* compatibility *) - if not (is_global (lib_ref "core.eq.type") eq) && - not (is_global (lib_ref "core.identity.type") eq) + if not (Constr.isRefX (lib_ref "core.eq.type") eq) && + not (Constr.isRefX (lib_ref "core.identity.type") eq) then raise Constr_matching.PatternMatchingFailure exception FoundHyp of (Id.t * constr * bool) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index c5ed02e043..5404404af5 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -431,10 +431,10 @@ let match_eq sigma eqn (ref, hetero) = in match EConstr.kind sigma eqn with | App (c, [|t; x; y|]) -> - if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y) + if not hetero && isRefX sigma ref c then PolymorphicLeibnizEq (t, x, y) else raise PatternMatchingFailure | App (c, [|t; x; t'; x'|]) -> - if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x') + if hetero && isRefX sigma ref c then HeterogenousEq (t, x, t', x') else raise PatternMatchingFailure | _ -> raise PatternMatchingFailure @@ -479,9 +479,9 @@ let find_this_eq_data_decompose env sigma eqn = let match_sigma env sigma ex = match EConstr.kind sigma ex with - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sig.intro") f -> + | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sig.intro") f -> build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) - | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (lib_ref "core.sigT.intro") f -> + | App (f, [| a; p; car; cdr |]) when isRefX sigma (lib_ref "core.sigT.intro") f -> build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure diff --git a/tactics/inv.ml b/tactics/inv.ml index 2181eb25af..4239fc8bc0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -352,7 +352,7 @@ let dest_nf_eq env sigma t = match EConstr.kind sigma t with | App (r, [| t; x; y |]) -> let open Reductionops in let eq = Coqlib.lib_ref "core.eq.type" in - if EConstr.is_global sigma eq r then + if isRefX sigma eq r then (t, whd_all env sigma x, whd_all env sigma y) else user_err Pp.(str "Not an equality.") | _ -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 609b752716..2d900a237a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3955,7 +3955,7 @@ let specialize_eqs id = match EConstr.kind !evars ty with | Prod (na, t, b) -> (match EConstr.kind !evars t with - | App (eq, [| eqty; x; y |]) when EConstr.is_global !evars Coqlib.(lib_ref "core.eq.type") eq -> + | App (eq, [| eqty; x; y |]) when isRefX !evars Coqlib.(lib_ref "core.eq.type") eq -> let c = if noccur_between !evars 1 (List.length ctx) x then y else x in let pt = mkApp (eq, [| eqty; c; c |]) in let ind = destInd !evars eq in @@ -3963,7 +3963,7 @@ let specialize_eqs id = if unif (push_rel_context ctx env) evars pt t then aux true ctx (mkApp (acc, [| p |])) (subst1 p b) else acc, in_eqs, ctx, ty - | App (heq, [| eqty; x; eqty'; y |]) when EConstr.is_global !evars (Lazy.force coq_heq_ref) heq -> + | App (heq, [| eqty; x; eqty'; y |]) when isRefX !evars (Lazy.force coq_heq_ref) heq -> let eqt, c = if noccur_between !evars 1 (List.length ctx) x then eqty', y else eqty, x in let pt = mkApp (heq, [| eqt; c; eqt; c |]) in let ind = destInd !evars heq in @@ -4134,8 +4134,8 @@ let compute_elim_sig sigma ?elimc elimt = | Some (LocalDef _) -> error_ind_scheme "" | Some (LocalAssum (_,ind)) -> let indhd,indargs = decompose_app sigma ind in - try {!res with indref = Some (fst (Termops.global_of_constr sigma indhd)) } - with e when CErrors.noncritical e -> + try {!res with indref = Some (fst (destRef sigma indhd)) } + with DestKO -> error "Cannot find the inductive type of the inductive scheme." let compute_scheme_signature evd scheme names_info ind_type_guess = diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v deleted file mode 100644 index fbd9c8bcba..0000000000 --- a/test-suite/failure/Template.v +++ /dev/null @@ -1,28 +0,0 @@ - -Module TestUnsetTemplateCheck. - Unset Template Check. - - Section Foo. - - Context (A : Type). - - Definition cstr := nat : ltac:(let ty := type of A in exact ty). - - Inductive myind := - | cons : A -> myind. - End Foo. - - (* Can only succeed if no template check is performed *) - Check myind True : Prop. - - About myind. - - (* test discharge puts things in the right order (by using the - checker on the result) *) - Section S. - - Variables (A:Type) (a:A). - Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B. - End S. - -End TestUnsetTemplateCheck. diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out index 6879cbc3c2..60bc9cbf55 100644 --- a/test-suite/output/Fixpoint.out +++ b/test-suite/output/Fixpoint.out @@ -1,8 +1,8 @@ -fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : -list B := match l with - | nil => nil - | a :: l0 => f a :: F A B f l0 - end +fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := + match l with + | nil => nil + | a :: l0 => f a :: F A B f l0 + end : forall A B : Set, (A -> B) -> list A -> list B let fix f (m : nat) : nat := match m with | 0 => 0 diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 3f4d5ef58c..190c34262f 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -3,6 +3,10 @@ foo : nat Axioms: foo : nat Axioms: +bli : Type +Axioms: +bli : Type +Axioms: extensionality : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index 3d4dfe603d..4c980fddba 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -30,6 +30,21 @@ Module P := N M. Print Assumptions M.bar. (* Should answer: foo *) Print Assumptions P.bar. (* Should answer: foo *) +(* Print Assumptions used empty instances on polymorphic inductives *) +Module Poly. + + Set Universe Polymorphism. + Axiom bli : Type. + + Definition bla := bli -> bli. + + Inductive blo : bli -> Type := . + + Print Assumptions bla. + Print Assumptions blo. + +End Poly. + (* The original test-case of the bug-report *) diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 745cf950b5..950c784325 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -9,9 +9,8 @@ (************************************************************************) open Format -open Coqdep_lexer -open Coqdep_common open Minisys +open Coqdep_common (** The basic parts of coqdep (i.e. the parts used by [coqdep -boot]) are now in [Coqdep_common]. The code that remains here concerns @@ -29,47 +28,6 @@ open Minisys let option_sort = ref false -let warning_mult suf iter = - let tab = Hashtbl.create 151 in - let check f d = - begin try - let d' = Hashtbl.find tab f in - if (Filename.dirname (file_name f d)) - <> (Filename.dirname (file_name f d')) then begin - coqdep_warning "the file %s is defined twice!" (f ^ suf) - end - with Not_found -> () end; - Hashtbl.add tab f d - in - iter check - -let sort () = - let seen = Hashtbl.create 97 in - let rec loop file = - let file = canonize file in - if not (Hashtbl.mem seen file) then begin - Hashtbl.add seen file (); - let cin = open_in (file ^ ".v") in - let lb = Lexing.from_channel cin in - try - while true do - match coq_action lb with - | Require (from, sl) -> - List.iter - (fun s -> - match search_v_known ?from s with - | None -> () - | Some f -> loop f) - sl - | _ -> () - done - with Fin_fichier -> - close_in cin; - printf "%s%s " file !suffixe - end - in - List.iter (fun (name,_) -> loop name) !vAccu - let usage () = eprintf " usage: coqdep [options] <filename>+\n"; eprintf " options:\n"; @@ -159,8 +117,6 @@ let coqdep () = List.iter (fun (f,d) -> add_mli_known f d ".mli") !mliAccu; List.iter (fun (f,d) -> add_mllib_known f d ".mllib") !mllibAccu; List.iter (fun (f,suff,d) -> add_ml_known f d suff) !mlAccu; - warning_mult ".mli" iter_mli_known; - warning_mult ".ml" iter_ml_known; if !option_sort then begin sort (); exit 0 end; if !option_c then mL_dependencies (); coq_dependencies (); diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index bd72a52adf..5ece595f13 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -125,8 +125,8 @@ let mkknown () = with Not_found -> None in add, iter, search -let add_ml_known, iter_ml_known, search_ml_known = mkknown () -let add_mli_known, iter_mli_known, search_mli_known = mkknown () +let add_ml_known, _, search_ml_known = mkknown () +let add_mli_known, _, search_mli_known = mkknown () let add_mllib_known, _, search_mllib_known = mkknown () let add_mlpack_known, _, search_mlpack_known = mkknown () @@ -616,3 +616,30 @@ let rec treat_file old_dirname old_name = | (base,".mlpack") -> addQueue mlpackAccu (base,dirname) | _ -> ()) | _ -> () + +let sort () = + let seen = Hashtbl.create 97 in + let rec loop file = + let file = canonize file in + if not (Hashtbl.mem seen file) then begin + Hashtbl.add seen file (); + let cin = open_in (file ^ ".v") in + let lb = Lexing.from_channel cin in + try + while true do + match coq_action lb with + | Require (from, sl) -> + List.iter + (fun s -> + match search_v_known ?from s with + | None -> () + | Some f -> loop f) + sl + | _ -> () + done + with Fin_fichier -> + close_in cin; + printf "%s%s " file !suffixe + end + in + List.iter (fun (name,_) -> loop name) !vAccu diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 96266b8e36..1820db4a1e 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -20,44 +20,34 @@ val coqdep_warning : ('a, Format.formatter, unit, unit) format4 -> 'a twice.*) val find_dir_logpath: string -> string list +(** Options *) val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref - val write_vos : bool ref -(** output vos and vok dependencies *) +val suffixe : string ref type dynlink = Opt | Byte | Both | No | Variable - val option_dynlink : dynlink ref + val norec_dirs : StrSet.t ref -val suffixe : string ref + type dir = string option -val get_extension : string -> string list -> string * string -val basename_noext : string -> string +val treat_file : dir -> string -> unit + +(** ML-related manipulation *) val mlAccu : (string * string * dir) list ref val mliAccu : (string * dir) list ref val mllibAccu : (string * dir) list ref -val vAccu : (string * string) list ref -val addQueue : 'a list ref -> 'a -> unit val add_ml_known : string -> dir -> string -> unit -val iter_ml_known : (string -> dir -> unit) -> unit -val search_ml_known : string -> dir option val add_mli_known : string -> dir -> string -> unit -val iter_mli_known : (string -> dir -> unit) -> unit -val search_mli_known : string -> dir option val add_mllib_known : string -> dir -> string -> unit -val search_mllib_known : string -> dir option -val search_v_known : ?from:string list -> string list -> string option -val file_name : string -> string option -> string -val escape : string -> string -val canonize : string -> string val mL_dependencies : unit -> unit + val coq_dependencies : unit -> unit -val suffixes : 'a list -> 'a list list val add_known : bool -> string -> string list -> string -> unit val add_coqlib_known : bool -> string -> string list -> string -> unit -val add_caml_known : string -> string list -> string -> unit + val add_caml_dir : string -> unit (** Simply add this directory and imports it, no subdirs. This is used @@ -73,5 +63,4 @@ val add_rec_dir_no_import : val add_rec_dir_import : (bool -> string -> string list -> string -> unit) -> string -> string list -> unit -val treat_file : dir -> string -> unit -val error_cannot_parse : string -> int * int -> 'a +val sort : unit -> unit diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 7d919956e8..506a8dc5b0 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -32,10 +32,6 @@ let set_type_in_type () = let typing_flags = Environ.typing_flags (Global.env ()) in Global.set_typing_flags { typing_flags with Declarations.check_universes = false } -let set_no_template_check () = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_template = false } - (******************************************************************************) type color = [`ON | `AUTO | `EMACS | `OFF] @@ -526,7 +522,6 @@ let parse_args ~help ~init arglist : t * string list = |"-list-tags" -> set_query oval PrintTags |"-time" -> { oval with config = { oval.config with time = true }} |"-type-in-type" -> set_type_in_type (); oval - |"-no-template-check" -> set_no_template_check (); oval |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false) |"-where" -> set_query oval PrintWhere |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp help) diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 051638d53c..6848862603 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -81,7 +81,6 @@ let print_usage_common co command = \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\n -no-template-check disable checking of universes constraints on universes parameterizing template polymorphic inductive types\ \n -mangle-names x mangle auto-generated names using prefix x\ \n -set \"Foo Bar\" enable Foo Bar (as Set Foo Bar. in a file)\ \n -set \"Foo Bar=value\" set Foo Bar to value (value is interpreted according to Foo Bar's type)\ diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index dacef1cb18..fb61a1089f 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -240,8 +240,16 @@ and traverse_inductive (curr, data, ax2ty) mind obj = (* Build the context of all arities *) let arities_ctx = let global_env = Global.env () in + let instance = + let open Univ in + Instance.of_array + (Array.init + (AUContext.size + (Declareops.inductive_polymorphic_context mib)) + Level.var) + in Array.fold_left (fun accu oib -> - let pspecif = Univ.in_punivs (mib, oib) in + let pspecif = ((mib, oib), instance) in let ind_type = Inductive.type_of_inductive global_env pspecif in let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in @@ -356,8 +364,5 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu in - if not mind.mind_typing_flags.check_template then - let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in - ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu - else accu + accu in GlobRef.Map_env.fold fold graph ContextObjectMap.empty diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 8de1c69424..dce0a70f72 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -323,16 +323,15 @@ let check_named {CAst.loc;v=na} = match na with let msg = str "Parameters must be named." in user_err ?loc msg -let template_polymorphism_candidate ~template_check ~ctor_levels uctx params concl = +let template_polymorphism_candidate ~ctor_levels uctx params concl = match uctx with | Entries.Monomorphic_entry uctx -> let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in if not concltemplate then false - else if not template_check then true else let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in let params, conclunivs = - IndTyping.template_polymorphic_univs ~template_check ~ctor_levels uctx params conclu + IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu in not (Univ.LSet.is_empty conclunivs) | Entries.Polymorphic_entry _ -> false @@ -385,7 +384,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames List.fold_left (fun levels c -> add_levels c levels) param_levels ctypes in - template_polymorphism_candidate ~template_check:(Environ.check_template env_ar_params) ~ctor_levels uctx ctx_params concl + template_polymorphism_candidate ~ctor_levels uctx ctx_params concl in let template = match template with | Some template -> diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index cc104b3762..1286e4a5c3 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -76,17 +76,15 @@ val should_auto_template : Id.t -> bool -> bool inductive under consideration. *) val template_polymorphism_candidate - : template_check:bool - -> ctor_levels:Univ.LSet.t + : ctor_levels:Univ.LSet.t -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool -(** [template_polymorphism_candidate ~template_check ~ctor_levels uctx params +(** [template_polymorphism_candidate ~ctor_levels uctx params conclsort] is [true] iff an inductive with params [params], conclusion [conclsort] and universe levels appearing in the constructor arguments [ctor_levels] would be definable as template polymorphic. It should have at least one universe in its monomorphic universe context that can be made parametric in its - conclusion sort, if one is given. If the [template_check] flag is - false we just check that the conclusion sort is not small. *) + conclusion sort, if one is given. *) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 17c3e0395a..dfc4631572 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j = str "because this term is not a type." let explain_reference_variables sigma id c = - (* c is intended to be a global reference *) - let pc = pr_global (fst (Termops.global_of_constr sigma c)) in - pc ++ strbrk " depends on the variable " ++ Id.print id ++ + pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++ strbrk " which is not declared in the context." let rec pr_disjunction pr = function diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 62ba6b157a..32c438c724 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -211,12 +211,10 @@ let pr_template_variables = function let print_polymorphism ref = let poly = Global.is_polymorphic ref in let template_poly = Global.is_template_polymorphic ref in - let template_checked = Global.is_template_checked ref in let template_variables = Global.get_template_polymorphic_variables ref in [ pr_global ref ++ str " is " ++ (if poly then str "universe polymorphic" else if template_poly then - (if not template_checked then str "assumed " else mt()) ++ str "template universe polymorphic " ++ h 0 (pr_template_variables template_variables) else str "not universe polymorphic") ] diff --git a/vernac/record.ml b/vernac/record.ml index df9b4a0914..f6945838d7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -446,8 +446,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa univs) param_levels fields in - let template_check = Environ.check_template (Global.env ()) in - ComInductive.template_polymorphism_candidate ~template_check ~ctor_levels univs params + ComInductive.template_polymorphism_candidate ~ctor_levels univs params (Some (Sorts.sort_of_univ min_univ)) in match template with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0fd47b8da1..fd588f5b15 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -609,24 +609,6 @@ let vernac_assumption ~atts discharge kind l nl = | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l -let set_template_check b = - let typing_flags = Environ.typing_flags (Global.env ()) in - Global.set_typing_flags { typing_flags with Declarations.check_template = b } - -let is_template_check () = - let typing_flags = Environ.typing_flags (Global.env ()) in - typing_flags.Declarations.check_template - -let () = - let tccheck = - { optdepr = true; - optname = "Template universe check"; - optkey = ["Template"; "Check"]; - optread = (fun () -> is_template_check ()); - optwrite = (fun b -> set_template_check b)} - in - declare_bool_option tccheck - let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false ~name:"Polymorphic inductive cumulativity" |