diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 7 | ||||
| -rw-r--r-- | kernel/cemitcodes.ml | 2 | ||||
| -rw-r--r-- | kernel/clambda.ml | 6 | ||||
| -rw-r--r-- | kernel/cooking.ml | 22 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 5 | ||||
| -rw-r--r-- | kernel/environ.ml | 21 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | kernel/inductive.ml | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 114 | ||||
| -rw-r--r-- | kernel/names.mli | 255 | ||||
| -rw-r--r-- | kernel/nativecode.ml | 14 | ||||
| -rw-r--r-- | kernel/reduction.ml | 45 | ||||
| -rw-r--r-- | kernel/term.ml | 256 | ||||
| -rw-r--r-- | kernel/term.mli | 396 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 34 | ||||
| -rw-r--r-- | kernel/typeops.ml | 10 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 |
19 files changed, 107 insertions, 1091 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 4da5f0f38..1d8861cbc 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1051,7 +1051,12 @@ let norm_val info tab v = let inject c = mk_clos (subs_id 0) c -let whd_stack infos tab m stk = +let whd_stack infos tab m stk = match m.norm with +| Whnf | Norm -> + (** No need to perform [kni] nor to unlock updates because + every head subterm of [m] is [Whnf] or [Norm] *) + knh infos m stk +| Red | Cstr -> let k = kni infos tab m stk in let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index cea09c510..f4e6d45c2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -13,7 +13,7 @@ (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) open Names -open Term +open Constr open Cbytecodes open Copcodes open Mod_subst diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 8389dd326..b722e4200 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -708,12 +708,10 @@ let rec lambda_of_constr env c = Lcofix(init, (names, ltypes, lbodies)) | Proj (p,c) -> - let kn = Projection.constant p in - let cb = lookup_constant kn env.global_env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p env.global_env in let n = pb.proj_arg in let lc = lambda_of_constr env c in - Lproj (n,kn,lc) + Lproj (n,Projection.constant p,lc) and lambda_of_app env f args = match Constr.kind f with diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 6f4541e95..5783453e6 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -227,28 +227,10 @@ let cook_constant ~hcons env { from = cb; info } = hyps) hyps ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let projection pb = - let c' = abstract_constant_body (expmod pb.proj_body) hyps in - let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in - let etat = abstract_constant_body (expmod (snd pb.proj_eta)) hyps in - let ((mind, _), _), n' = - try - let c' = share_univs cache (IndRef (pb.proj_ind,0)) Univ.Instance.empty modlist in - match kind c' with - | App (f,l) -> (destInd f, Array.length l) - | Ind ind -> ind, 0 - | _ -> assert false - with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) - in - let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in - { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; - proj_eta = etab, etat; - proj_type = ty'; proj_body = c' } - in { cook_body = body; cook_type = typ; - cook_proj = Option.map projection cb.const_proj; + cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7bd0ae566..0d907f3de 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : projection_body option; + cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index b7427d20a..913c13173 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -87,7 +87,7 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : projection_body option; + const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 832d478b3..75c0e5b4c 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -94,14 +94,13 @@ let subst_const_body sub cb = else let body' = subst_const_def sub cb.const_body in let type' = subst_const_type sub cb.const_type in - let proj' = Option.Smart.map (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type - && proj' == cb.const_proj then cb + then cb else { const_hyps = []; const_body = body'; const_type = type'; - const_proj = proj'; + const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/environ.ml b/kernel/environ.ml index c3e7cec75..fb89576dd 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -108,6 +109,7 @@ let empty_rel_context_val = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; @@ -485,14 +487,10 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) let polymorphic_ind (mind,i) env = @@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = diff --git a/kernel/environ.mli b/kernel/environ.mli index fc45ce0e3..8928b32f1 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -48,6 +48,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9bed598bb..090acdf16 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -803,9 +803,7 @@ let rec subterm_specif renv stack t = (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) - let kn = Projection.constant p in - let cb = lookup_constant kn renv.env in - let pb = Option.get cb.const_proj in + let pb = lookup_projection p renv.env in let n = pb.proj_arg in spec_of_tree (List.nth wf_args n) | Dead_code -> Dead_code diff --git a/kernel/names.ml b/kernel/names.ml index 58d311dd5..54f089e60 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -760,55 +760,8 @@ let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 (*******************************************************************) (** Compatibility layers *) -(** Backward compatibility for [Id] *) - -type identifier = Id.t - -let id_eq = Id.equal -let id_ord = Id.compare -let string_of_id = Id.to_string -let id_of_string = Id.of_string - -module Idset = Id.Set -module Idmap = Id.Map -module Idpred = Id.Pred - -(** Compatibility layer for [Name] *) - -let name_eq = Name.equal - -(** Compatibility layer for [DirPath] *) - -type dir_path = DirPath.t -let dir_path_ord = DirPath.compare -let dir_path_eq = DirPath.equal -let make_dirpath = DirPath.make -let repr_dirpath = DirPath.repr -let empty_dirpath = DirPath.empty -let is_empty_dirpath = DirPath.is_empty -let string_of_dirpath = DirPath.to_string -let initial_dir = DirPath.initial - -(** Compatibility layer for [MBId] *) - type mod_bound_id = MBId.t -let mod_bound_id_ord = MBId.compare -let mod_bound_id_eq = MBId.equal -let make_mbid = MBId.make -let repr_mbid = MBId.repr -let debug_string_of_mbid = MBId.debug_to_string -let string_of_mbid = MBId.to_string -let id_of_mbid = MBId.to_id - -(** Compatibility layer for [Label] *) - -type label = Id.t -let mk_label = Label.make -let string_of_label = Label.to_string -let pr_label = Label.print -let id_of_label = Label.to_id -let label_of_id = Label.of_id -let eq_label = Label.equal +let eq_constant_key = Constant.UserOrd.equal (** Compatibility layer for [ModPath] *) @@ -816,32 +769,13 @@ type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of module_path * Label.t -let check_bound_mp = ModPath.is_bound -let string_of_mp = ModPath.to_string -let mp_ord = ModPath.compare -let mp_eq = ModPath.equal -let initial_path = ModPath.initial - -(** Compatibility layer for [KerName] *) - -type kernel_name = KerName.t -let make_kn = KerName.make -let repr_kn = KerName.repr -let modpath = KerName.modpath -let label = KerName.label -let string_of_kn = KerName.to_string -let pr_kn = KerName.print -let kn_ord = KerName.compare (** Compatibility layer for [Constant] *) -type constant = Constant.t - +module Projection = +struct + type t = Constant.t * bool -module Projection = -struct - type t = constant * bool - let make c b = (c, b) let constant = fst @@ -906,6 +840,9 @@ module GlobRef = struct end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + type evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Constant.t @@ -915,40 +852,3 @@ let eq_egr e1 e2 = match e1, e2 with EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2 | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2 | _, _ -> false - -let constant_of_kn = Constant.make1 -let constant_of_kn_equiv = Constant.make -let make_con = Constant.make3 -let repr_con = Constant.repr3 -let canonical_con = Constant.canonical -let user_con = Constant.user -let con_label = Constant.label -let con_modpath = Constant.modpath -let eq_constant = Constant.equal -let eq_constant_key = Constant.UserOrd.equal -let con_ord = Constant.CanOrd.compare -let con_user_ord = Constant.UserOrd.compare -let string_of_con = Constant.to_string -let pr_con = Constant.print -let debug_string_of_con = Constant.debug_to_string -let debug_pr_con = Constant.debug_print -let con_with_label = Constant.change_label - -(** Compatibility layer for [MutInd] *) - -type mutual_inductive = MutInd.t -let mind_of_kn = MutInd.make1 -let mind_of_kn_equiv = MutInd.make -let make_mind = MutInd.make3 -let canonical_mind = MutInd.canonical -let user_mind = MutInd.user -let repr_mind = MutInd.repr3 -let mind_label = MutInd.label -let mind_modpath = MutInd.modpath -let eq_mind = MutInd.equal -let mind_ord = MutInd.CanOrd.compare -let mind_user_ord = MutInd.UserOrd.compare -let string_of_mind = MutInd.to_string -let pr_mind = MutInd.print -let debug_string_of_mind = MutInd.debug_to_string -let debug_pr_mind = MutInd.debug_print diff --git a/kernel/names.mli b/kernel/names.mli index 566fcd0f9..f988b559a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -538,116 +538,8 @@ val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) -(** {5 Identifiers} *) - -type identifier = Id.t -[@@ocaml.deprecated "Alias for [Id.t]"] - -val string_of_id : Id.t -> string -[@@ocaml.deprecated "Same as [Id.to_string]."] - -val id_of_string : string -> Id.t -[@@ocaml.deprecated "Same as [Id.of_string]."] - -val id_ord : Id.t -> Id.t -> int -[@@ocaml.deprecated "Same as [Id.compare]."] - -val id_eq : Id.t -> Id.t -> bool -[@@ocaml.deprecated "Same as [Id.equal]."] - -module Idset : Set.S with type elt = Id.t and type t = Id.Set.t -[@@ocaml.deprecated "Same as [Id.Set]."] - -module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t -[@@ocaml.deprecated "Same as [Id.Pred]."] - -module Idmap : module type of Id.Map -[@@ocaml.deprecated "Same as [Id.Map]."] - -(** {5 Directory paths} *) - -type dir_path = DirPath.t -[@@ocaml.deprecated "Alias for [DirPath.t]."] - -val dir_path_ord : DirPath.t -> DirPath.t -> int -[@@ocaml.deprecated "Same as [DirPath.compare]."] - -val dir_path_eq : DirPath.t -> DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.equal]."] - -val make_dirpath : module_ident list -> DirPath.t -[@@ocaml.deprecated "Same as [DirPath.make]."] - -val repr_dirpath : DirPath.t -> module_ident list -[@@ocaml.deprecated "Same as [DirPath.repr]."] - -val empty_dirpath : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.empty]."] - -val is_empty_dirpath : DirPath.t -> bool -[@@ocaml.deprecated "Same as [DirPath.is_empty]."] - -val string_of_dirpath : DirPath.t -> string -[@@ocaml.deprecated "Same as [DirPath.to_string]."] - -val initial_dir : DirPath.t -[@@ocaml.deprecated "Same as [DirPath.initial]."] - -(** {5 Labels} *) - -type label = Label.t -[@@ocaml.deprecated "Same as [Label.t]."] -(** Alias type *) - -val mk_label : string -> Label.t -[@@ocaml.deprecated "Same as [Label.make]."] - -val string_of_label : Label.t -> string -[@@ocaml.deprecated "Same as [Label.to_string]."] - -val pr_label : Label.t -> Pp.t -[@@ocaml.deprecated "Same as [Label.print]."] - -val label_of_id : Id.t -> Label.t -[@@ocaml.deprecated "Same as [Label.of_id]."] - -val id_of_label : Label.t -> Id.t -[@@ocaml.deprecated "Same as [Label.to_id]."] - -val eq_label : Label.t -> Label.t -> bool -[@@ocaml.deprecated "Same as [Label.equal]."] - -(** {5 Unique bound module names} *) - type mod_bound_id = MBId.t [@@ocaml.deprecated "Same as [MBId.t]."] - -val mod_bound_id_ord : MBId.t -> MBId.t -> int -[@@ocaml.deprecated "Same as [MBId.compare]."] - -val mod_bound_id_eq : MBId.t -> MBId.t -> bool -[@@ocaml.deprecated "Same as [MBId.equal]."] - -val make_mbid : DirPath.t -> Id.t -> MBId.t -[@@ocaml.deprecated "Same as [MBId.make]."] - -val repr_mbid : MBId.t -> int * Id.t * DirPath.t -[@@ocaml.deprecated "Same as [MBId.repr]."] - -val id_of_mbid : MBId.t -> Id.t -[@@ocaml.deprecated "Same as [MBId.to_id]."] - -val string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.to_string]."] - -val debug_string_of_mbid : MBId.t -> string -[@@ocaml.deprecated "Same as [MBId.debug_to_string]."] - -(** {5 Names} *) - -val name_eq : Name.t -> Name.t -> bool -[@@ocaml.deprecated "Same as [Name.equal]."] - (** {5 Module paths} *) type module_path = ModPath.t = @@ -656,52 +548,6 @@ type module_path = ModPath.t = | MPdot of ModPath.t * Label.t [@@ocaml.deprecated "Alias type"] -val mp_ord : ModPath.t -> ModPath.t -> int -[@@ocaml.deprecated "Same as [ModPath.compare]."] - -val mp_eq : ModPath.t -> ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.equal]."] - -val check_bound_mp : ModPath.t -> bool -[@@ocaml.deprecated "Same as [ModPath.is_bound]."] - -val string_of_mp : ModPath.t -> string -[@@ocaml.deprecated "Same as [ModPath.to_string]."] - -val initial_path : ModPath.t -[@@ocaml.deprecated "Same as [ModPath.initial]."] - -(** {5 Kernel names} *) - -type kernel_name = KerName.t -[@@ocaml.deprecated "Alias type"] - -val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t -[@@ocaml.deprecated "Same as [KerName.make]."] - -val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [KerName.repr]."] - -val modpath : KerName.t -> ModPath.t -[@@ocaml.deprecated "Same as [KerName.modpath]."] - -val label : KerName.t -> Label.t -[@@ocaml.deprecated "Same as [KerName.label]."] - -val string_of_kn : KerName.t -> string -[@@ocaml.deprecated "Same as [KerName.to_string]."] - -val pr_kn : KerName.t -> Pp.t -[@@ocaml.deprecated "Same as [KerName.print]."] - -val kn_ord : KerName.t -> KerName.t -> int -[@@ocaml.deprecated "Same as [KerName.compare]."] - -(** {5 Constant names} *) - -type constant = Constant.t -[@@ocaml.deprecated "Alias type"] - module Projection : sig type t @@ -749,6 +595,9 @@ module GlobRef : sig end +type global_reference = GlobRef.t +[@@ocaml.deprecated "Alias for [GlobRef.t]"] + (** Better to have it here that in Closure, since required in grammar.cma *) (* XXX: Move to a module *) type evaluable_global_reference = @@ -756,101 +605,3 @@ type evaluable_global_reference = | EvalConstRef of Constant.t val eq_egr : evaluable_global_reference -> evaluable_global_reference -> bool - -val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make]"] - -val constant_of_kn : KerName.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make1]"] - -val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.make3]"] - -val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [Constant.repr3]"] - -val user_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.user]"] - -val canonical_con : Constant.t -> KerName.t -[@@ocaml.deprecated "Same as [Constant.canonical]"] - -val con_modpath : Constant.t -> ModPath.t -[@@ocaml.deprecated "Same as [Constant.modpath]"] - -val con_label : Constant.t -> Label.t -[@@ocaml.deprecated "Same as [Constant.label]"] - -val eq_constant : Constant.t -> Constant.t -> bool -[@@ocaml.deprecated "Same as [Constant.equal]"] - -val con_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.CanOrd.compare]"] - -val con_user_ord : Constant.t -> Constant.t -> int -[@@ocaml.deprecated "Same as [Constant.UserOrd.compare]"] - -val con_with_label : Constant.t -> Label.t -> Constant.t -[@@ocaml.deprecated "Same as [Constant.change_label]"] - -val string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.to_string]"] - -val pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.print]"] - -val debug_pr_con : Constant.t -> Pp.t -[@@ocaml.deprecated "Same as [Constant.debug_print]"] - -val debug_string_of_con : Constant.t -> string -[@@ocaml.deprecated "Same as [Constant.debug_to_string]"] - -(** {5 Mutual Inductive names} *) - -type mutual_inductive = MutInd.t -[@@ocaml.deprecated "Alias type"] - -val mind_of_kn : KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make1]"] - -val mind_of_kn_equiv : KerName.t -> KerName.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make]"] - -val make_mind : ModPath.t -> DirPath.t -> Label.t -> MutInd.t -[@@ocaml.deprecated "Same as [MutInd.make3]"] - -val user_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.user]"] - -val canonical_mind : MutInd.t -> KerName.t -[@@ocaml.deprecated "Same as [MutInd.canonical]"] - -val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t -[@@ocaml.deprecated "Same as [MutInd.repr3]"] - -val eq_mind : MutInd.t -> MutInd.t -> bool -[@@ocaml.deprecated "Same as [MutInd.equal]"] - -val mind_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.CanOrd.compare]"] - -val mind_user_ord : MutInd.t -> MutInd.t -> int -[@@ocaml.deprecated "Same as [MutInd.UserOrd.compare]"] - -val mind_label : MutInd.t -> Label.t -[@@ocaml.deprecated "Same as [MutInd.label]"] - -val mind_modpath : MutInd.t -> ModPath.t -[@@ocaml.deprecated "Same as [MutInd.modpath]"] - -val string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.to_string]"] - -val pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.print]"] - -val debug_pr_mind : MutInd.t -> Pp.t -[@@ocaml.deprecated "Same as [MutInd.debug_print]"] - -val debug_string_of_mind : MutInd.t -> string -[@@ocaml.deprecated "Same as [MutInd.debug_to_string]"] diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 0cd0ad46c..036cd4847 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1859,7 +1859,7 @@ and compile_named env sigma univ auxdefs id = let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with - | None -> + | false -> let no_univs = match cb.const_universes with | Monomorphic_const _ -> true @@ -1903,7 +1903,8 @@ let compile_constant env sigma prefix ~interactive con cb = if interactive then LinkedInteractive prefix else Linked prefix end - | Some pb -> + | true -> + let pb = lookup_projection (Projection.make con false) env in let mind = pb.proj_ind in let ind = (mind,0) in let mib = lookup_mind mind env in @@ -2029,11 +2030,12 @@ let rec compile_deps env sigma prefix ~interactive init t = else let comp_stack, (mind_updates, const_updates) = match cb.const_proj, cb.const_body with - | None, Def t -> + | false, Def t -> compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) - | Some pb, _ -> - let mind = pb.proj_ind in - compile_mind_deps env prefix ~interactive init mind + | true, _ -> + let pb = lookup_projection (Projection.make c false) env in + let mind = pb.proj_ind in + compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 8ca596d48..f4af31386 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -648,25 +648,24 @@ let check_leq univs u u' = let check_sort_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if not (type_in_type env) then + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> () (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> () (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible | (Prop c1, Type u) -> - if not (type_in_type env) then - let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> check_leq univs u0 u - | CONV -> check_eq univs u0 u) + let u0 = univ_of_sort s0 in + (match pb with + | CUMUL -> check_leq univs u0 u + | CONV -> check_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> check_leq univs u1 u2 - | CONV -> check_eq univs u1 u2) + (match pb with + | CUMUL -> check_leq univs u1 u2 + | CONV -> check_eq univs u1 u2) let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs @@ -699,25 +698,25 @@ let infer_leq (univs, cstrs as cuniv) u u' = let infer_cmp_universes env pb s0 s1 univs = let open Sorts in - match (s0,s1) with + if type_in_type env then univs + else + match (s0,s1) with | (Prop c1, Prop c2) when is_cumul pb -> begin match c1, c2 with - | Null, _ | _, Pos -> univs (* Prop <= Set *) - | _ -> raise NotConvertible + | Null, _ | _, Pos -> univs (* Prop <= Set *) + | _ -> raise NotConvertible end | (Prop c1, Prop c2) -> if c1 == c2 then univs else raise NotConvertible | (Prop c1, Type u) -> let u0 = univ_of_sort s0 in - (match pb with - | CUMUL -> infer_leq univs u0 u - | CONV -> infer_eq univs u0 u) + (match pb with + | CUMUL -> infer_leq univs u0 u + | CONV -> infer_eq univs u0 u) | (Type u, Prop c) -> raise NotConvertible | (Type u1, Type u2) -> - if not (type_in_type env) then - (match pb with - | CUMUL -> infer_leq univs u1 u2 - | CONV -> infer_eq univs u1 u2) - else univs + (match pb with + | CUMUL -> infer_leq univs u1 u2 + | CONV -> infer_eq univs u1 u2) let infer_convert_instances ~flex u u' (univs,cstrs) = let cstrs' = diff --git a/kernel/term.ml b/kernel/term.ml index e1affb1c0..b44e038e9 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -15,219 +15,17 @@ open Names open Vars open Constr -(**********************************************************************) -(** Redeclaration of types from module Constr *) -(**********************************************************************) - +(* Deprecated *) type contents = Sorts.contents = Pos | Null - -type sorts = Sorts.t = - | Prop of contents (** Prop and Set *) - | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.contents"] type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] -type constr = Constr.t -(** Alias types, for compatibility. *) - -type types = Constr.t -(** Same as [constr], for documentation purposes. *) - -type existential_key = Evar.t -type existential = Constr.existential - -type metavariable = Constr.metavariable - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : case_style } - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : case_printing - } - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast - -(********************************************************************) -(* Constructions as implemented *) -(********************************************************************) - -type rec_declaration = Constr.rec_declaration -type fixpoint = Constr.fixpoint -type cofixpoint = Constr.cofixpoint -type 'constr pexistential = 'constr Constr.pexistential -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -type 'a puniverses = 'a Univ.puniverses - -(** Simply type aliases *) -type pconstant = Constant.t puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of metavariable - | Evar of 'constr pexistential - | Sort of 'sort - | Cast of 'constr * cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) pfixpoint - | CoFix of ('constr, 'types) pcofixpoint - | Proj of Projection.t * 'constr - -type values = Vmvalues.values - -(**********************************************************************) -(** Redeclaration of functions from module Constr *) -(**********************************************************************) - -let set_sort = Sorts.set -let prop_sort = Sorts.prop -let type1_sort = Sorts.type1 -let sorts_ord = Sorts.compare -let is_prop_sort = Sorts.is_prop -let family_of_sort = Sorts.family -let univ_of_sort = Sorts.univ_of_sort -let sort_of_univ = Sorts.sort_of_univ - -(** {6 Term constructors. } *) - -let mkRel = Constr.mkRel -let mkVar = Constr.mkVar -let mkMeta = Constr.mkMeta -let mkEvar = Constr.mkEvar -let mkSort = Constr.mkSort -let mkProp = Constr.mkProp -let mkSet = Constr.mkSet -let mkType = Constr.mkType -let mkCast = Constr.mkCast -let mkProd = Constr.mkProd -let mkLambda = Constr.mkLambda -let mkLetIn = Constr.mkLetIn -let mkApp = Constr.mkApp -let mkConst = Constr.mkConst -let mkProj = Constr.mkProj -let mkInd = Constr.mkInd -let mkConstruct = Constr.mkConstruct -let mkConstU = Constr.mkConstU -let mkIndU = Constr.mkIndU -let mkConstructU = Constr.mkConstructU -let mkConstructUi = Constr.mkConstructUi -let mkCase = Constr.mkCase -let mkFix = Constr.mkFix -let mkCoFix = Constr.mkCoFix - -(**********************************************************************) -(** Aliases of functions from module Constr *) -(**********************************************************************) - -let eq_constr = Constr.equal -let eq_constr_univs = Constr.eq_constr_univs -let leq_constr_univs = Constr.leq_constr_univs -let eq_constr_nounivs = Constr.eq_constr_nounivs - -let kind_of_term = Constr.kind -let compare = Constr.compare -let constr_ord = compare -let fold_constr = Constr.fold -let map_puniverses = Constr.map_puniverses -let map_constr = Constr.map -let map_constr_with_binders = Constr.map_with_binders -let iter_constr = Constr.iter -let iter_constr_with_binders = Constr.iter_with_binders -let compare_constr = Constr.compare_head -let hash_constr = Constr.hash -let hcons_sorts = Sorts.hcons -let hcons_constr = Constr.hcons -let hcons_types = Constr.hcons - -(**********************************************************************) -(** HERE BEGINS THE INTERESTING STUFF *) -(**********************************************************************) - -(**********************************************************************) -(* Non primitive term destructors *) -(**********************************************************************) - -exception DestKO = DestKO -(* Destructs a de Bruijn index *) -let destRel = destRel -let destMeta = destRel -let isMeta = isMeta -let destVar = destVar -let isSort = isSort -let destSort = destSort -let isprop = isprop -let is_Prop = is_Prop -let is_Set = is_Set -let is_Type = is_Type -let is_small = is_small -let iskind = iskind -let isEvar = isEvar -let isEvar_or_Meta = isEvar_or_Meta -let destCast = destCast -let isCast = isCast -let isRel = isRel -let isRelN = isRelN -let isVar = isVar -let isVarId = isVarId -let isInd = isInd -let destProd = destProd -let isProd = isProd -let destLambda = destLambda -let isLambda = isLambda -let destLetIn = destLetIn -let isLetIn = isLetIn -let destApp = destApp -let destApplication = destApp -let isApp = isApp -let destConst = destConst -let isConst = isConst -let destEvar = destEvar -let destInd = destInd -let destConstruct = destConstruct -let isConstruct = isConstruct -let destCase = destCase -let isCase = isCase -let isProj = isProj -let destProj = destProj -let destFix = destFix -let isFix = isFix -let destCoFix = destCoFix -let isCoFix = isCoFix - -(******************************************************************) -(* Flattening and unflattening of embedded applications and casts *) -(******************************************************************) - -let decompose_app c = - match kind_of_term c with - | App (f,cl) -> (f, Array.to_list cl) - | _ -> (c,[]) - -let decompose_appvect c = - match kind_of_term c with - | App (f,cl) -> (f, cl) - | _ -> (c,[||]) +type sorts = Sorts.t = + | Prop of Sorts.contents (** Prop and Set *) + | Type of Univ.Universe.t (** Type *) +[@@ocaml.deprecated "Alias for Sorts.t"] (****************************************************************************) (* Functions for dealing with constr terms *) @@ -321,7 +119,7 @@ let rec to_lambda n prod = if Int.equal n 0 then prod else - match kind_of_term prod with + match kind prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c | _ -> user_err ~hdr:"to_lambda" (mt ()) @@ -330,7 +128,7 @@ let rec to_prod n lam = if Int.equal n 0 then lam else - match kind_of_term lam with + match kind lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c | _ -> user_err ~hdr:"to_prod" (mt ()) @@ -342,7 +140,7 @@ let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) let lambda_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Lambda(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough lambda's.") in @@ -355,7 +153,7 @@ let lambda_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -367,7 +165,7 @@ let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = - match kind_of_term c, l with + match kind c, l with | Prod(_,_,c), arg::l -> app (arg::subst) c l | _, [] -> substl subst c | _ -> anomaly (Pp.str "Not enough prod's.") in @@ -381,7 +179,7 @@ let prod_applist_assum n c l = if Int.equal n 0 then if l == [] then substl subst t else anomaly (Pp.str "Too many arguments.") - else match kind_of_term t, l with + else match kind t, l with | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l | _, [] -> anomaly (Pp.str "Not enough arguments.") @@ -397,7 +195,7 @@ let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) let decompose_prod = - let rec prodec_rec l c = match kind_of_term c with + let rec prodec_rec l c = match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c @@ -407,7 +205,7 @@ let decompose_prod = (* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam = - let rec lamdec_rec l c = match kind_of_term c with + let rec lamdec_rec l c = match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c @@ -420,7 +218,7 @@ let decompose_prod_n n = if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> user_err (str "decompose_prod_n: not enough products") @@ -433,7 +231,7 @@ let decompose_lam_n n = if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with + else match kind c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> user_err (str "decompose_lam_n: not enough abstractions") @@ -445,7 +243,7 @@ let decompose_lam_n n = let decompose_prod_assum = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c @@ -458,7 +256,7 @@ let decompose_prod_assum = let decompose_lam_assum = let rec lamdec_rec l c = let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c @@ -477,7 +275,7 @@ let decompose_prod_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c @@ -498,7 +296,7 @@ let decompose_lam_n_assum n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c @@ -514,7 +312,7 @@ let decompose_lam_n_decls n = if Int.equal n 0 then l,c else let open Context.Rel.Declaration in - match kind_of_term c with + match kind c with | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c @@ -541,12 +339,12 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * sorts +type arity = Context.Rel.t * Sorts.t let destArity = let open Context.Rel.Declaration in let rec prodec_rec l c = - match kind_of_term c with + match kind c with | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c @@ -558,7 +356,7 @@ let destArity = let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign let rec isArity c = - match kind_of_term c with + match kind c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) | Cast (c,_,_) -> isArity c @@ -569,13 +367,13 @@ let rec isArity c = (* Experimental, used in Presburger contrib *) type ('constr, 'types) kind_of_type = - | SortType of sorts + | SortType of Sorts.t | CastType of 'types * 'types | ProdType of Name.t * 'types * 'types | LetInType of Name.t * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array -let kind_of_type t = match kind_of_term t with +let kind_of_type t = match kind t with | Sort s -> SortType s | Cast (c,_,t) -> CastType (c, t) | Prod (na,t,c) -> ProdType (na, t, c) diff --git a/kernel/term.mli b/kernel/term.mli index ee84dcb2b..f651d1a58 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -11,166 +11,6 @@ open Names open Constr -(** {5 Redeclaration of types from module Constr and Sorts} - - This reexports constructors of inductive types defined in module [Constr], - for compatibility purposes. Refer to this module for further info. - -*) - -exception DestKO -[@@ocaml.deprecated "Alias for [Constr.DestKO]"] - -(** {5 Simple term case analysis. } *) -val isRel : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRel]"] -val isRelN : int -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isRelN]"] -val isVar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVar]"] -val isVarId : Id.t -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isVarId]"] -val isInd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isInd]"] -val isEvar : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar]"] -val isMeta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isMeta]"] -val isEvar_or_Meta : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isEvar_or_Meta]"] -val isSort : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isSort]"] -val isCast : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCast]"] -val isApp : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isApp]"] -val isLambda : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isLambda]"] -val isLetIn : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isletIn]"] -val isProd : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProp]"] -val isConst : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConst]"] -val isConstruct : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isConstruct]"] -val isFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isFix]"] -val isCoFix : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCoFix]"] -val isCase : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isCase]"] -val isProj : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isProj]"] - -val is_Prop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Prop]"] -val is_Set : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Set]"] -val isprop : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.isprop]"] -val is_Type : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_Type]"] -val iskind : constr -> bool -[@@ocaml.deprecated "Alias for [Constr.is_kind]"] -val is_small : Sorts.t -> bool -[@@ocaml.deprecated "Alias for [Constr.is_small]"] - - -(** {5 Term destructors } *) -(** Destructor operations are partial functions and - @raise DestKO if the term has not the expected form. *) - -(** Destructs a de Bruijn index *) -val destRel : constr -> int -[@@ocaml.deprecated "Alias for [Constr.destRel]"] - -(** Destructs an existential variable *) -val destMeta : constr -> metavariable -[@@ocaml.deprecated "Alias for [Constr.destMeta]"] - -(** Destructs a variable *) -val destVar : constr -> Id.t -[@@ocaml.deprecated "Alias for [Constr.destVar]"] - -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) -val destSort : constr -> Sorts.t -[@@ocaml.deprecated "Alias for [Constr.destSort]"] - -(** Destructs a casted term *) -val destCast : constr -> constr * cast_kind * constr -[@@ocaml.deprecated "Alias for [Constr.destCast]"] - -(** Destructs the product {% $ %}(x:t_1)t_2{% $ %} *) -val destProd : types -> Name.t * types * types -[@@ocaml.deprecated "Alias for [Constr.destProd]"] - -(** Destructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) -val destLambda : constr -> Name.t * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLambda]"] - -(** Destructs the let {% $ %}[x:=b:t_1]t_2{% $ %} *) -val destLetIn : constr -> Name.t * constr * types * constr -[@@ocaml.deprecated "Alias for [Constr.destLetIn]"] - -(** Destructs an application *) -val destApp : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApp]"] - -(** Obsolete synonym of destApp *) -val destApplication : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destApplication]"] - -(** Decompose any term as an applicative term; the list of args can be empty *) -val decompose_app : constr -> constr * constr list -[@@ocaml.deprecated "Alias for [Constr.decompose_app]"] - -(** Same as [decompose_app], but returns an array. *) -val decompose_appvect : constr -> constr * constr array -[@@ocaml.deprecated "Alias for [Constr.decompose_appvect]"] - -(** Destructs a constant *) -val destConst : constr -> Constant.t Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConst]"] - -(** Destructs an existential variable *) -val destEvar : constr -> existential -[@@ocaml.deprecated "Alias for [Constr.destEvar]"] - -(** Destructs a (co)inductive type *) -val destInd : constr -> inductive Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destInd]"] - -(** Destructs a constructor *) -val destConstruct : constr -> constructor Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.destConstruct]"] - -(** Destructs a [match c as x in I args return P with ... | -Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args -return P in t1], or [if c then t1 else t2]) -@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] -where [info] is pretty-printing information *) -val destCase : constr -> case_info * constr * constr * constr array -[@@ocaml.deprecated "Alias for [Constr.destCase]"] - -(** Destructs a projection *) -val destProj : constr -> Projection.t * constr -[@@ocaml.deprecated "Alias for [Constr.destProj]"] - -(** Destructs the {% $ %}i{% $ %}th function of the block - [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} - with f{_ 2} ctx{_ 2} = b{_ 2} - ... - with f{_ n} ctx{_ n} = b{_ n}], - where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. -*) -val destFix : constr -> fixpoint -[@@ocaml.deprecated "Alias for [Constr.destFix]"] - -val destCoFix : constr -> cofixpoint -[@@ocaml.deprecated "Alias for [Constr.destCoFix]"] - (** {5 Derived constructors} *) (** non-dependent product [t1 -> t2], an alias for @@ -349,242 +189,14 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type -(** {5 Redeclaration of stuff from module [Sorts]} *) - -val set_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.set"] - -val prop_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.prop"] - -val type1_sort : Sorts.t -[@@ocaml.deprecated "Alias for Sorts.type1"] - -val sorts_ord : Sorts.t -> Sorts.t -> int -[@@ocaml.deprecated "Alias for Sorts.compare"] - -val is_prop_sort : Sorts.t -> bool -[@@ocaml.deprecated "Alias for Sorts.is_prop"] - -val family_of_sort : Sorts.t -> Sorts.family -[@@ocaml.deprecated "Alias for Sorts.family"] - -(** {5 Redeclaration of stuff from module [Constr]} - - See module [Constr] for further info. *) - -(** {6 Term constructors. } *) - -val mkRel : int -> constr -[@@ocaml.deprecated "Alias for Constr.mkRel"] -val mkVar : Id.t -> constr -[@@ocaml.deprecated "Alias for Constr.mkVar"] -val mkMeta : metavariable -> constr -[@@ocaml.deprecated "Alias for Constr.mkMeta"] -val mkEvar : existential -> constr -[@@ocaml.deprecated "Alias for Constr.mkEvar"] -val mkSort : Sorts.t -> types -[@@ocaml.deprecated "Alias for Constr.mkSort"] -val mkProp : types -[@@ocaml.deprecated "Alias for Constr.mkProp"] -val mkSet : types -[@@ocaml.deprecated "Alias for Constr.mkSet"] -val mkType : Univ.Universe.t -> types -[@@ocaml.deprecated "Alias for Constr.mkType"] -val mkCast : constr * cast_kind * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProd : Name.t * types * types -> types -[@@ocaml.deprecated "Alias for Constr"] -val mkLambda : Name.t * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkLetIn : Name.t * constr * types * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkApp : constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConst : Constant.t -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkProj : Projection.t * constr -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkInd : inductive -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstruct : constructor -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstU : Constant.t Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkIndU : inductive Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructU : constructor Univ.puniverses -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkConstructUi : (pinductive * int) -> constr -[@@ocaml.deprecated "Alias for Constr"] -val mkCase : case_info * constr * constr * constr array -> constr -[@@ocaml.deprecated "Alias for Constr.mkCase"] -val mkFix : fixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkFix"] -val mkCoFix : cofixpoint -> constr -[@@ocaml.deprecated "Alias for Constr.mkCoFix"] - -(** {6 Aliases} *) - -val eq_constr : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.equal"] - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [u]. *) -val eq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.eq_constr_univs"] - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [u]. *) -val leq_constr_univs : constr UGraph.check_function -[@@ocaml.deprecated "Alias for Constr.leq_constr_univs"] - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool -[@@ocaml.deprecated "Alias for Constr.qe_constr_nounivs"] - -val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term -[@@ocaml.deprecated "Alias for Constr.kind"] - -val compare : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Constr.compare]"] - -val constr_ord : constr -> constr -> int -[@@ocaml.deprecated "Alias for [Term.compare]"] - -val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a -[@@ocaml.deprecated "Alias for [Constr.fold]"] - -val map_constr : (constr -> constr) -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map]"] - -val map_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr -[@@ocaml.deprecated "Alias for [Constr.map_with_binders]"] - -val map_puniverses : ('a -> 'b) -> 'a Univ.puniverses -> 'b Univ.puniverses -[@@ocaml.deprecated "Alias for [Constr.map_puniverses]"] -val univ_of_sort : Sorts.t -> Univ.Universe.t -[@@ocaml.deprecated "Alias for [Sorts.univ_of_sort]"] -val sort_of_univ : Univ.Universe.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.sort_of_univ]"] - -val iter_constr : (constr -> unit) -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter]"] - -val iter_constr_with_binders : - ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit -[@@ocaml.deprecated "Alias for [Constr.iter_with_binders]"] - -val compare_constr : (int -> constr -> constr -> bool) -> int -> constr -> constr -> bool -[@@ocaml.deprecated "Alias for [Constr.compare_head]"] - -type constr = Constr.constr -[@@ocaml.deprecated "Alias for Constr.t"] - -(** Alias types, for compatibility. *) - -type types = Constr.types -[@@ocaml.deprecated "Alias for Constr.types"] - +(* Deprecated *) type contents = Sorts.contents = Pos | Null [@@ocaml.deprecated "Alias for Sorts.contents"] +type sorts_family = Sorts.family = InProp | InSet | InType +[@@ocaml.deprecated "Alias for Sorts.family"] + type sorts = Sorts.t = | Prop of Sorts.contents (** Prop and Set *) | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] - -type sorts_family = Sorts.family = InProp | InSet | InType -[@@ocaml.deprecated "Alias for Sorts.family"] - -type 'a puniverses = 'a Univ.puniverses -[@@ocaml.deprecated "Alias for Constr.puniverses"] - -(** Simply type aliases *) -type pconstant = Constr.pconstant -[@@ocaml.deprecated "Alias for Constr.pconstant"] -type pinductive = Constr.pinductive -[@@ocaml.deprecated "Alias for Constr.pinductive"] -type pconstructor = Constr.pconstructor -[@@ocaml.deprecated "Alias for Constr.pconstructor"] -type existential_key = Evar.t -[@@ocaml.deprecated "Alias for Evar.t"] -type existential = Constr.existential -[@@ocaml.deprecated "Alias for Constr.existential"] -type metavariable = Constr.metavariable -[@@ocaml.deprecated "Alias for Constr.metavariable"] - -type case_style = Constr.case_style = - LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle -[@@ocaml.deprecated "Alias for Constr.case_style"] - -type case_printing = Constr.case_printing = - { ind_tags : bool list; cstr_tags : bool list array; style : Constr.case_style } -[@@ocaml.deprecated "Alias for Constr.case_printing"] - -type case_info = Constr.case_info = - { ci_ind : inductive; - ci_npar : int; - ci_cstr_ndecls : int array; - ci_cstr_nargs : int array; - ci_pp_info : Constr.case_printing - } -[@@ocaml.deprecated "Alias for Constr.case_info"] - -type cast_kind = Constr.cast_kind = - VMcast | NATIVEcast | DEFAULTcast | REVERTcast -[@@ocaml.deprecated "Alias for Constr.cast_kind"] - -type rec_declaration = Constr.rec_declaration -[@@ocaml.deprecated "Alias for Constr.rec_declaration"] -type fixpoint = Constr.fixpoint -[@@ocaml.deprecated "Alias for Constr.fixpoint"] -type cofixpoint = Constr.cofixpoint -[@@ocaml.deprecated "Alias for Constr.cofixpoint"] -type 'constr pexistential = 'constr Constr.pexistential -[@@ocaml.deprecated "Alias for Constr.pexistential"] -type ('constr, 'types) prec_declaration = - ('constr, 'types) Constr.prec_declaration -[@@ocaml.deprecated "Alias for Constr.prec_declaration"] -type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint -[@@ocaml.deprecated "Alias for Constr.pfixpoint"] -type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint -[@@ocaml.deprecated "Alias for Constr.pcofixpoint"] - -type ('constr, 'types, 'sort, 'univs) kind_of_term = - ('constr, 'types, 'sort, 'univs) Constr.kind_of_term = - | Rel of int - | Var of Id.t - | Meta of Constr.metavariable - | Evar of 'constr Constr.pexistential - | Sort of 'sort - | Cast of 'constr * Constr.cast_kind * 'types - | Prod of Name.t * 'types * 'types - | Lambda of Name.t * 'types * 'constr - | LetIn of Name.t * 'constr * 'types * 'constr - | App of 'constr * 'constr array - | Const of (Constant.t * 'univs) - | Ind of (inductive * 'univs) - | Construct of (constructor * 'univs) - | Case of Constr.case_info * 'constr * 'constr * 'constr array - | Fix of ('constr, 'types) Constr.pfixpoint - | CoFix of ('constr, 'types) Constr.pcofixpoint - | Proj of Projection.t * 'constr -[@@ocaml.deprecated "Alias for Constr.kind_of_term"] - -type values = Vmvalues.values -[@@ocaml.deprecated "Alias for Vmvalues.values"] - -val hash_constr : Constr.constr -> int -[@@ocaml.deprecated "Alias for Constr.hash"] - -val hcons_sorts : Sorts.t -> Sorts.t -[@@ocaml.deprecated "Alias for [Sorts.hcons]"] - -val hcons_constr : Constr.constr -> Constr.constr -[@@ocaml.deprecated "Alias for [Constr.hcons]"] - -val hcons_types : Constr.types -> Constr.types -[@@ocaml.deprecated "Alias for [Constr.hcons]"] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 7352c1882..db1109e75 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +291,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,7 +343,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = None; + cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -370,7 +370,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); cook_type = typ; - cook_proj = Some pb; + cook_proj = true; cook_universes = univs; cook_inline = false; cook_context = None; @@ -458,30 +458,8 @@ let build_constant_declaration kn env result = check declared inferred) lc) in let univs = result.cook_universes in let tps = - let res = - match result.cook_proj with - | None -> Cbytegen.compile_constant_body ~fail_on_error:false env univs def - | Some pb -> - (* The compilation of primitive projections is a bit tricky, because - they refer to themselves (the body of p looks like fun c => - Proj(p,c)). We break the cycle by building an ad-hoc compilation - environment. A cleaner solution would be that kernel projections are - simply Proj(i,c) with i an int and c a constr, but we would have to - get rid of the compatibility layer. *) - let cb = - { const_hyps = hyps; - const_body = def; - const_type = typ; - const_proj = result.cook_proj; - const_body_code = None; - const_universes = univs; - const_inline_code = result.cook_inline; - const_typing_flags = Environ.typing_flags env; - } - in - let env = add_constant kn cb env in - Cbytegen.compile_constant_body ~fail_on_error:false env univs def - in Option.map Cemitcodes.from_val res + let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in + Option.map Cemitcodes.from_val res in { const_hyps = hyps; const_body = def; diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fd9cefb2c..325d5cecd 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -528,13 +528,3 @@ let judge_of_case env ci pj cj lfj = let lf, lft = dest_judgev lfj in make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) - -let type_of_projection_constant env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if Declareops.constant_is_polymorphic cb then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 85b2cfffd..546f2d2b4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -100,8 +100,6 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Projection.t puniverses -> types - val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) |