diff options
Diffstat (limited to 'kernel')
33 files changed, 511 insertions, 935 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 810c346990..94ca4c72dd 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -299,7 +299,7 @@ and pp_bytecodes c = | Ksequence (l1, l2) :: c -> pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> - tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c + pp_instr i ++ fnl () ++ pp_bytecodes c (*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index b1fc0c85de..57b397e6f8 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -979,7 +979,7 @@ let compile fail_on_error ?universes:(universes=0) env c = Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ; Some (init_code,!fun_code, Array.of_list fv) with TooLargeInductive tname -> - let fn = if fail_on_error then CErrors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index f13620e101..40c1e027d4 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -24,33 +24,45 @@ type reloc_info = type patch = reloc_info * int let patch_char4 buff pos c1 c2 c3 c4 = - String.unsafe_set buff pos c1; - String.unsafe_set buff (pos + 1) c2; - String.unsafe_set buff (pos + 2) c3; - String.unsafe_set buff (pos + 3) c4 + Bytes.unsafe_set buff pos c1; + Bytes.unsafe_set buff (pos + 1) c2; + Bytes.unsafe_set buff (pos + 2) c3; + Bytes.unsafe_set buff (pos + 3) c4 let patch buff (pos, n) = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) +(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) let patch_int buff patches = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) - let buff = String.copy buff in + let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - buff + (* Note: we follow the apporach suggested by Gabriel Scherer in + PR#136 here, and use unsafe as we own buff. + + The crux of the question that avoids defining emitcodes just as a + Byte.t is the call to hcons in to_memory below. Even if disabling + this optimization has no visible time impact, test data shows + that the optimization is indeed triggered quite often so we + choose ugliness over altering the semantics. + + Handle with care. + *) + Bytes.unsafe_to_string buff (* Buffering of bytecode *) -let out_buffer = ref(String.create 1024) +let out_buffer = ref(Bytes.create 1024) and out_position = ref 0 let out_word b1 b2 b3 b4 = let p = !out_position in - if p >= String.length !out_buffer then begin - let len = String.length !out_buffer in + if p >= Bytes.length !out_buffer then begin + let len = Bytes.length !out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 = if len = Sys.max_string_length then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in - let new_buffer = String.create new_len in - String.blit !out_buffer 0 new_buffer 0 len; + let new_buffer = Bytes.create new_len in + Bytes.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; patch_char4 !out_buffer p (Char.unsafe_chr b1) @@ -94,10 +106,10 @@ let extend_label_table needed = let backpatch (pos, orig) = let displ = (!out_position - orig) asr 2 in - !out_buffer.[pos] <- Char.unsafe_chr displ; - !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8); - !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16); - !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24) + Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) let define_label lbl = if lbl >= Array.length !label_table then extend_label_table lbl; @@ -308,7 +320,7 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = string +type emitcodes = String.t let length = String.length @@ -372,9 +384,8 @@ let to_memory (init_code, fun_code, fv) = init(); emit init_code []; emit fun_code []; - let code = String.create !out_position in - String.unsafe_blit !out_buffer 0 code 0 !out_position; (** Later uses of this string are all purely functional *) + let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> diff --git a/kernel/constr.mli b/kernel/constr.mli index 42d298e3b9..7095dbe6f9 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -189,8 +189,12 @@ type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type ('constr, 'types) kind_of_term = - | Rel of int - | Var of Id.t + | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) + + | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends + the local context of the currently open section + (i.e. [Variable] or [Let]). *) + | Meta of metavariable | Evar of 'constr pexistential | Sort of Sorts.t @@ -199,12 +203,16 @@ type ('constr, 'types) kind_of_term = | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. + The {!mkApp} constructor also enforces the following invariant: - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + + | Const of constant puniverses (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) + + | Ind of inductive puniverses (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Construct of constructor puniverses (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint diff --git a/kernel/context.ml b/kernel/context.ml index 4e53b73a28..ae0388003d 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -138,7 +138,7 @@ struct | LocalDef (_,v,ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = + let fold_constr f decl acc = match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) @@ -147,9 +147,6 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) end (** Rel-context is represented as a list of declarations. @@ -336,7 +333,7 @@ struct | LocalDef (_, v, ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = + let fold_constr f decl a = match decl with | LocalAssum (_, ty) -> f ty a | LocalDef (_, v, ty) -> a |> f v |> f ty @@ -348,6 +345,18 @@ struct let of_tuple = function | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + + let of_rel_decl f = function + | Rel.Declaration.LocalAssum (na,t) -> + LocalAssum (f na, t) + | Rel.Declaration.LocalDef (na,v,t) -> + LocalDef (f na, v, t) + + let to_rel_decl = function + | LocalAssum (id,t) -> + Rel.Declaration.LocalAssum (Name id, t) + | LocalDef (id,v,t) -> + Rel.Declaration.LocalDef (Name id,v,t) end (** Named-context is represented as a list of declarations. @@ -401,23 +410,39 @@ struct | _ -> None in List.map_filter filter - end +end -module NamedList = +module Compacted = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t - - let map_constr f (ids, copt, ty as decl) = - let copt' = Option.map f copt in - let ty' = f ty in - if copt == copt' && ty == ty' then decl else (ids, copt', ty') + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + + let map_constr f = function + | LocalAssum (ids, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (ids, ty') + | LocalDef (ids, c, ty) as decl -> + let ty' = f ty in + let c' = f c in + if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') + + let of_named_decl = function + | Named.Declaration.LocalAssum (id,t) -> + LocalAssum ([id],t) + | Named.Declaration.LocalDef (id,v,t) -> + LocalDef ([id],v,t) + + let to_named_context = function + | LocalAssum (ids, t) -> + List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids + | LocalDef (ids, v, t) -> + List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end type t = Declaration.t list let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index b5f3904d22..955e214cb9 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -79,10 +79,9 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Name.t * Constr.t option * Constr.t - val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -193,10 +192,18 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Id.t * Constr.t option * Constr.t val of_tuple : Id.t * Constr.t option * Constr.t -> t + + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. + The function provided as the first parameter determines how to translate "names" to "ids". *) + val of_rel_decl : (Name.t -> Id.t) -> Rel.Declaration.t -> t + + (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *) + (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *) + val to_rel_decl : t -> Rel.Declaration.t end (** Rel-context is represented as a list of declarations. @@ -244,17 +251,20 @@ sig val to_instance : t -> Constr.t list end -module NamedList : +module Compacted : sig module Declaration : sig - type t = Id.t list * Constr.t option * Constr.t + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + val map_constr : (Constr.t -> Constr.t) -> t -> t + val of_named_decl : Named.Declaration.t -> t + val to_named_context : t -> Named.t end type t = Declaration.t list val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a end - -type section_context = Named.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1345991503..f5059cd750 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,8 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with @@ -152,7 +154,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } = in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 327e697d23..eb40730969 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,7 +19,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option val cook_constant : env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index c27cb04870..40595f944c 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let open Context.Named in - let open Declaration in - env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let open Context.Rel in - let open Declaration in - env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f89773fcc5..7821ea20ff 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -58,10 +58,11 @@ type projection_body = { proj_body : constr; (* For compatibility with VMs only, the match version *) } +(* Global declarations (i.e. constants) can be either: *) type constant_def = - | Undef of inline - | Def of constr Mod_subst.substituted - | OpaqueDef of Opaqueproof.opaque + | Undef of inline (** a global assumption *) + | Def of constr Mod_subst.substituted (** or a transparent global definition *) + | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = Univ.universe_context @@ -78,7 +79,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { - const_hyps : Context.section_context; (** New: younger hyp at top *) + const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; @@ -177,7 +178,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e062a..0a822d6fad 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,7 +9,8 @@ open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -146,7 +147,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types let hcons_rel_context l = List.smartmap hcons_rel_decl l diff --git a/kernel/entries.mli b/kernel/entries.mli index ea7c266bcd..77081947ec 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.section_context option; + const_entry_secctx : Context.Named.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -73,7 +73,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.section_context option * bool * types Univ.in_universe_context * inline + Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { proj_entry_ind : mutual_inductive; diff --git a/kernel/environ.ml b/kernel/environ.ml index 16ddfac64b..4a543f1957 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -413,7 +413,7 @@ let global_vars_set env constr = Id.Set.union (vars_of_global env c) acc | _ -> acc in - fold_constr filtrec acc c + Term.fold_constr filtrec acc c in filtrec Id.Set.empty constr diff --git a/kernel/environ.mli b/kernel/environ.mli index 6ac00088b3..ea570cb4a8 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -231,7 +231,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml deleted file mode 100644 index bd91c689d2..0000000000 --- a/kernel/fast_typeops.ml +++ /dev/null @@ -1,463 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open CErrors -open Util -open Names -open Univ -open Term -open Vars -open Declarations -open Environ -open Reduction -open Inductive -open Type_errors - -let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y - -let conv_leq_vecti env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq false env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 - -let check_constraints cst env = - if Environ.check_constraints cst env then () - else error_unsatisfied_constraints env cst - -(* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - -let check_type env c t = - match kind_of_term(whd_all env t) with - | Sort s -> s - | _ -> error_not_type env (make_judge c t) - -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = - try let _ = check_type env t ty in t - with TypeError _ -> - error_assumption env (make_judge t ty) - -(************************************************) -(* Incremental typing rules: builds a typing judgment given the *) -(* judgments for the subterms. *) - -(*s Type of sorts *) - -(* Prop and Set *) - -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop - -(* Type of Type(i). *) - -let judge_of_type u = - let uu = Universe.super u in - mkType uu - -(*s Type of a de Bruijn index. *) - -let judge_of_relative env n = - try - let open Context.Rel.Declaration in - env |> lookup_rel n |> get_type |> lift n - with Not_found -> - error_unbound_rel env n - -(* Type of variables *) -let judge_of_variable env id = - try named_type id env - with Not_found -> - error_unbound_var env id - -(* Management of context of variables. *) - -(* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) -let check_hyps_inclusion env f c sign = - Context.Named.fold_outside - (fun decl () -> - let open Context.Named.Declaration in - let id = get_id decl in - let ty1 = get_type decl in - try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> - error_reference_variables env id (f c)) - sign - ~init:() - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -(* Type of constants *) - - -let type_of_constant_knowing_parameters_arity env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -(* Type of a lambda-abstraction. *) - -(* [judge_of_abstraction env name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let judge_of_abstraction env name var ty = - mkProd (name, var, ty) - -(* Type of an application. *) - -let make_judgev c t = - Array.map2 make_judge c t - -let judge_of_apply env func funt argsv argstv = - let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - - | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt - -(* Type of product *) - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) - -(* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ1 |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) -let judge_of_product env name s1 s2 = - let s = sort_of_product env s1 s2 in - mkSort s - -(* Type of a type cast *) - -(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule - - env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 - --------------------------------------------------------------------- - env |- c:typ2 -*) - -let judge_of_cast env c ct k expected_type = - try - match k with - | VMcast -> - vm_conv CUMUL env ct expected_type - | DEFAULTcast -> - default_conv ~l2r:false CUMUL env ct expected_type - | REVERTcast -> - default_conv ~l2r:true CUMUL env ct expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - Nativeconv.native_conv CUMUL sigma env ct expected_type - with NotConvertible -> - error_actual_type env (make_judge c ct) expected_type - -(* Inductive types. *) - -(* The type is parametric over the uniform parameters whose conclusion - is in Type; to enforce the internal constraints between the - parameters and the instances of Type occurring in the type of the - constructors, we use the level variables _statically_ assigned to - the conclusions of the parameters as mediators: e.g. if a parameter - has conclusion Type(alpha), static constraints of the form alpha<=v - exist between alpha and the Type's occurring in the constructor - types; when the parameters is finally instantiated by a term of - conclusion Type(u), then the constraints u<=alpha is computed in - the App case of execute; from this constraints, the expected - dynamic constraints of the form u<=v are enforced *) - -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args - in - check_constraints cst env; - t - -let judge_of_inductive env (ind,u as indu) = - let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t - -(* Constructors. *) - -let judge_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 in - let specif = lookup_mind_specif env (inductive_of_constructor c) in - let t,cst = constrained_type_of_constructor cu specif in - let () = check_constraints cst env in - t - -(* Case. *) - -let check_branch_types env (ind,u) c ct lft explft = - try conv_leq_vecti env lft explft - with - NotConvertibleVect i -> - error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) - | Invalid_argument _ -> - error_number_branches env (make_judge c ct) (Array.length explft) - -let judge_of_case env ci p pt c ct lf lft = - let (pind, _ as indspec) = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in - let (bty,rslty) = - type_case_branches env indspec (make_judge p pt) c in - let () = check_branch_types env pind c ct lft bty in - rslty - -let judge_of_projection env p c ct = - let pb = lookup_projection p env in - let (ind,u), args = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) - in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty - - -(* Fixpoints. *) - -(* Checks the type of a general (co)fixpoint, i.e. without checking *) -(* the specific guard condition. *) - -let type_fixpoint env lna lar vdef vdeft = - let lt = Array.length vdeft in - assert (Int.equal (Array.length lar) lt); - try - conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) - with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar - -(************************************************************************) -(************************************************************************) - -(* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - Ind et Constructsi un jour cela devient des constructions - arbitraires et non plus des variables *) -let rec execute env cstr = - let open Context.Rel.Declaration in - match kind_of_term cstr with - (* Atomic terms *) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> - judge_of_type u - - | Rel n -> - judge_of_relative env n - - | Var id -> - judge_of_variable env id - - | Const c -> - judge_of_constant env c - - | Proj (p, c) -> - let ct = execute env c in - judge_of_projection env p c ct - - (* Lambda calculus operators *) - | App (f,args) -> - let argst = execute_array env args in - let ft = - match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* Full or no sort-polymorphism *) - execute env f - in - - judge_of_apply env f ft args argst - - | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t - - | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - judge_of_product env name vars vars' - - | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t - - | Cast (c,k,t) -> - let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in - t - - (* Inductive types *) - | Ind ind -> - judge_of_inductive env ind - - | Construct c -> - judge_of_constructor env c - - | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft - - | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty - - | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty - - (* Partial proofs: unsupported by the kernel *) - | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") - - | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") - -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) - -(* Derived functions *) -let infer env constr = - let t = execute env constr in - make_judge constr t - -let infer = - if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - -let infer_type env constr = - execute_type env constr - -let infer_v env cv = - let jv = execute_array env cv in - make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 41cff607e7..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Environ -open Declarations - -(** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of - (local) universe variables (the ones that appear in the term) - and associated constraints. In case of polymorphic definitions, - these variables and constraints will be generalized. - *) - - -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9c..4c540a6d73 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing diff --git a/kernel/names.ml b/kernel/names.ml index 1eb9a31751..ee8d838da1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -50,17 +50,20 @@ struct | None -> true | Some _ -> false + let of_bytes s = + let s = Bytes.to_string s in + check_soft s; + String.hcons s + let of_string s = let () = check_soft s in - let s = String.copy s in String.hcons s let of_string_soft s = let () = check_soft ~warn:false s in - let s = String.copy s in String.hcons s - let to_string id = String.copy id + let to_string id = id let print id = str id @@ -88,11 +91,14 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false - let is_name = not % is_anonymous + let is_name = is_anonymous %> not let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -601,7 +607,13 @@ end module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env = HMap.Make(Constant.UserOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) + module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Cmap.Set module Cset_env = Cmap_env.Set diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775c..be9b9422b7 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -43,6 +43,7 @@ sig (** Check that a string may be converted to an identifier. @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) + val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. @@ -82,6 +83,9 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + (** constructor *) + val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *) @@ -368,8 +372,14 @@ end module Cpred : Predicate.S with type elt = Constant.t module Cset : CSig.SetS with type elt = Constant.t module Cset_env : CSig.SetS with type elt = Constant.t + module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) (** {6 Inductive names} *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index eaddace4b7..33bd7d8ddc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1848,10 +1848,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let open Context.Rel in - let n = length env.env_rel_context - n in - let open Declaration in - match lookup n env.env_rel_context with + let n = Context.Rel.length env.env_rel_context - n in + let open Context.Rel.Declaration in + match Context.Rel.lookup n env.env_rel_context with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e9..366f9a0a6d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,6 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr +module RelDecl = Context.Rel.Declaration + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -727,8 +729,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let open Context.Rel.Declaration in - let ids = List.rev_map get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1c58c7445c..6bd82170e6 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -35,7 +35,7 @@ let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) let include_dirs () = - [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] + [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 8093df3044..965ed67b07 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -491,12 +491,12 @@ let str_encode expr = let str_decode s = let mshl_expr_len = String.length s / 2 in let mshl_expr = Buffer.create mshl_expr_len in - let buf = String.create 2 in + let buf = Bytes.create 2 in for i = 0 to mshl_expr_len - 1 do - String.blit s (2*i) buf 0 2; - Buffer.add_char mshl_expr (bin_of_hex buf) + Bytes.blit_string s (2*i) buf 0 2; + Buffer.add_char mshl_expr (bin_of_hex (Bytes.to_string buf)) done; - Marshal.from_string (Buffer.contents mshl_expr) 0 + Marshal.from_bytes (Buffer.to_bytes mshl_expr) 0 (** Retroknowledge, to be removed when we switch to primitive integers *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 130f1eb039..f147ea3433 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -136,7 +136,7 @@ let dump (otab,_) = let disch_table = Array.make n a_discharge in let f2t_map = ref FMap.empty in Int.Map.iter (fun n (d,cu) -> - let c, u = Future.split2 ~greedy:true cu in + let c, u = Future.split2 cu in Future.sink u; Future.sink c; opaque_table.(n) <- c; diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index f211583e06..d14a254d32 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -17,7 +17,8 @@ open Util open Names open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -128,10 +129,10 @@ let env_of_rel n env = (* Named context *) let push_named_context_val_val d rval ctxt = -(* assert (not (Id.Map.mem (get_id d) ctxt.env_named_map)); *) +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) { env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (get_id d) (d, rval) ctxt.env_named_map; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; } let push_named_context_val d ctxt = @@ -140,8 +141,8 @@ let push_named_context_val d ctxt = let match_named_context_val c = match c.env_named_ctx with | [] -> None | decl :: ctx -> - let (_, v) = Id.Map.find (get_id decl) c.env_named_map in - let map = Id.Map.remove (get_id decl) c.env_named_map in + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in let cval = { env_named_ctx = ctx; env_named_map = map } in Some (decl, v, cval) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index bc1cb63d82..2312f891c5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -69,7 +71,7 @@ open Context.Named.Declaration - [env] : the underlying environment (cf Environ) - [modpath] : the current module name - [modvariant] : - * NONE before coqtop initialization (or when -notop is used) + * NONE before coqtop initialization * LIBRARY at toplevel of a compilation or a regular coqtop session * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] @@ -361,7 +363,7 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in @@ -795,7 +797,7 @@ type native_library = Nativecode.global list let get_library_native_symbols senv dir = try DPMap.find dir senv.native_symbols - with Not_found -> CErrors.errorlabstrm "get_library_native_symbols" + with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols" Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ (str "This use case is not supported, but disabling the native compiler may help.")) @@ -819,7 +821,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -855,7 +857,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err ~hdr:"Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in diff --git a/kernel/term.ml b/kernel/term.ml index 15f187e5c4..62c161be4c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -328,38 +328,9 @@ let destCoFix c = match kind_of_term c with let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false (******************************************************************) -(* Cast management *) -(******************************************************************) - -let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_,_) -> strip_outer_cast c - | _ -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) - -let under_outer_cast f c = match kind_of_term c with - | Cast (b,k,t) -> mkCast (f b, k, f t) - | _ -> f c - -let rec under_casts f c = match kind_of_term c with - | Cast (c,k,t) -> mkCast (under_casts f c, k, t) - | _ -> f c - -(******************************************************************) (* Flattening and unflattening of embedded applications and casts *) (******************************************************************) -(* flattens application lists throwing casts in-between *) -let collapse_appl c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = - match kind_of_term (strip_outer_cast f) with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | _ -> mkApp (f,cl2) - in - collapse_rec f cl - | _ -> c - let decompose_app c = match kind_of_term c with | App (f,cl) -> (f, Array.to_list cl) @@ -465,7 +436,7 @@ let rec to_lambda n prod = match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c - | _ -> errorlabstrm "to_lambda" (mt ()) + | _ -> user_err ~hdr:"to_lambda" (mt ()) let rec to_prod n lam = if Int.equal n 0 then @@ -474,7 +445,7 @@ let rec to_prod n lam = match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c - | _ -> errorlabstrm "to_prod" (mt ()) + | _ -> user_err ~hdr:"to_prod" (mt ()) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) diff --git a/kernel/term.mli b/kernel/term.mli index 60a3c77154..a8d9dfbfff 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** Flattens application lists *) -val collapse_appl : constr -> constr - - -(** Remove recursively the casts around a term i.e. - [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : constr -> constr - -(** Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(** Apply a function under components of Cast if any *) -val under_outer_cast : (constr -> constr) -> constr -> constr - (** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index b7597ba7fb..569a583780 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,9 @@ open Declarations open Environ open Entries open Typeops -open Fast_typeops + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) @@ -56,8 +58,7 @@ let inline_side_effects env body ctx side_eff = let cbl = List.filter not_exists cbl in let cname c = let name = string_of_con c in - for i = 0 to String.length name - 1 do - if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done; + let name = String.map (fun c -> if c == '.' || c == '#' then '_' else c) name in Name (id_of_string name) in let rec sub c i x = match kind_of_term x with | Const (c', _) when eq_constant c c' -> mkRel i @@ -175,7 +176,7 @@ let infer_declaration ~trust env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = - Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) -> + Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> let body, uctx, signatures = inline_side_effects env body uctx side_eff in let valid_signatures = check_signatures trust signatures in @@ -247,18 +248,17 @@ let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> Context.Rel.fold_outside - (Context.Rel.Declaration.fold + (RelDecl.fold_constr (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty let record_aux env s_ty s_bo suggested_expr = - let open Context.Named.Declaration in let in_ty = keep_hyps env s_ty in let v = String.concat " " (CList.map_filter (fun decl -> - let id = get_id decl in - if List.exists (Id.equal id % get_id) in_ty then None + let id = NamedDecl.get_id decl in + if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None else Some (Id.to_string id)) (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr) @@ -267,26 +267,25 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = - let open Context.Named.Declaration in let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in + let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - errorlabstrm "" (Pp.(str "The following section " ++ + user_err (Pp.(str "The following section " ++ str (String.plural n "variable") ++ str " " ++ str (String.conjugate_verb_to_be n) ++ str " used but not declared:" ++ fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in let sort evn l = List.filter (fun decl -> - let id = get_id decl in - List.exists (Names.Id.equal id % get_id) l) + let id = NamedDecl.get_id decl in + List.exists (NamedDecl.get_id %> Names.Id.equal id) l) (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in match ctx with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: @@ -414,7 +413,7 @@ let export_side_effects mb env ce = let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with - const_entry_body = Future.chain ~greedy:true ~pure:true body + const_entry_body = Future.chain ~pure:true body (fun (b_ctx, _) -> b_ctx, []) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false @@ -480,8 +479,7 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let open Context.Named.Declaration in - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Opaqueproof.force_proof (opaque_tables env) lc) in @@ -497,7 +495,7 @@ let translate_local_def mb env id centry = let translate_mind env kn mie = Indtypes.check_inductive env kn mie let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain ~greedy:true ~pure:true + const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in (body, ctx'), []); diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0059111c09..7d9a2aac09 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -14,11 +14,12 @@ open Term open Vars open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -35,61 +36,46 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) -let type_judgment env j = - match kind_of_term(whd_all env j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j +(* This should be a type (a priori without intention to be an assumption) *) +let check_type env c t = + match kind_of_term(whd_all env t) with + | Sort s -> s + | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env j = - try (type_judgment env j).utj_val +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = + try let _ = check_type env t ty in t with TypeError _ -> - error_assumption env j + error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) (* Prop and Set *) -let judge_of_prop = - { uj_val = mkProp; - uj_type = mkSort type1_sort } - -let judge_of_set = - { uj_val = mkSet; - uj_type = mkSort type1_sort } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in - { uj_val = mkType u; - uj_type = mkType uu } + mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try - let typ = get_type (lookup_rel n env) in - { uj_val = mkRel n; - uj_type = lift n typ } + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = - try - let ty = named_type id env in - make_judge (mkVar id) ty +let type_of_variable env id = + try named_type id env with Not_found -> error_unbound_var env id @@ -98,11 +84,11 @@ let judge_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 c sign = +let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in - let id = get_id d1 in + let id = NamedDecl.get_id d1 in try let d2 = lookup_named id env in conv env (get_type d2) (get_type d1); @@ -114,7 +100,7 @@ let check_hyps_inclusion env 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 c) + error_reference_variables env id (f c)) sign ~init:() @@ -122,35 +108,9 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | LocalAssum (_,p) -> extract_level env p :: l - | LocalDef _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t - (* Type of constants *) + let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t @@ -159,49 +119,28 @@ let type_of_constant_type_knowing_parameters env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu + let ty = type_of_constant_type_knowing_parameters env ty args in + let () = check_constraints cu env in + ty -let type_of_constant_knowing_parameters_in env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty paramtyps - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env ty args let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in - let ar = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ar [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let c = mkConstU cst in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - make_judge c ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -let type_of_projection env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") + type_of_constant_knowing_parameters_in env cst [||] +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -215,40 +154,36 @@ let type_of_projection env (p,u) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } - -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; - uj_type = subst1 defj.uj_val j.uj_type } +let type_of_abstraction env name var ty = + mkProd (name, var, ty) (* Type of an application. *) -let judge_of_apply env funj argjv = - let rec apply_rec n typ = function - | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } - | hj::restjl -> - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - (try - let () = conv_leq false env hj.uj_type c1 in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - with NotConvertible -> - error_cant_apply_bad_type env - (n,c1, hj.uj_type) - funj argjv) - - | _ -> - error_cant_apply_not_functional env funj argjv) - in - apply_rec 1 - funj.uj_type - (Array.to_list argjv) +let make_judgev c t = + Array.map2 make_judge c t + +let type_of_apply env func funt argsv argstv = + let len = Array.length argsv in + let rec apply_rec i typ = + if Int.equal i len then typ + else + (match kind_of_term (whd_all env typ) with + | Prod (_,c1,c2) -> + let arg = argsv.(i) and argt = argstv.(i) in + (try + let () = conv_leq false env argt c1 in + apply_rec (i+1) (subst1 arg c2) + with NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv)) + + | _ -> + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv)) + in apply_rec 0 funt (* Type of product *) @@ -281,10 +216,9 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name t1 t2 = - let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s } +let type_of_product env name s1 s2 = + let s = sort_of_product env s1 s2 in + mkSort s (* Type of a type cast *) @@ -295,29 +229,20 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj k tj = - let expected_type = tj.utj_val in +let check_cast env c ct k expected_type = try - let c, cst = - match k with - | VMcast -> - mkCast (cj.uj_val, k, expected_type), - Reduction.vm_conv CUMUL env cj.uj_type expected_type - | DEFAULTcast -> - mkCast (cj.uj_val, k, expected_type), - default_conv ~l2r:false CUMUL env cj.uj_type expected_type - | REVERTcast -> - cj.uj_val, - default_conv ~l2r:true CUMUL env cj.uj_type expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - mkCast (cj.uj_val, k, expected_type), - Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type - in - { uj_val = c; - uj_type = expected_type } + match k with + | VMcast -> + vm_conv CUMUL env ct expected_type + | DEFAULTcast -> + default_conv ~l2r:false CUMUL env ct expected_type + | REVERTcast -> + default_conv ~l2r:true CUMUL env ct expected_type + | NATIVEcast -> + let sigma = Nativelambda.empty_evars in + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> - error_actual_type env cj expected_type + error_actual_type env (make_judge c ct) expected_type (* Inductive types. *) @@ -333,83 +258,78 @@ let judge_of_cast env cj k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let c = mkIndU indu in +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; + check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - make_judge c t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = - let c = mkIndU indu in - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in - check_constraints cst env; - (make_judge c t) +let type_of_inductive env (ind,u as indu) = + let (mib,mip) = lookup_mind_specif env ind in + check_hyps_inclusion env mkIndU indu mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let constr = mkConstructU cu in - let _ = +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 constr mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu 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 let () = check_constraints cst env in - (make_judge constr t) + t (* Case. *) -let check_branch_types env (ind,u) cj (lfj,explft) = - try conv_leq_vecti env (Array.map j_type lfj) explft +let check_branch_types env (ind,u) c ct lft explft = + try conv_leq_vecti env lft explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) | Invalid_argument _ -> - error_number_branches env cj (Array.length explft) + error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci pj cj lfj = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj in + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in let () = check_case_info env pind ci in let (bty,rslty) = - type_case_branches env indspec pj cj.uj_val in - let () = check_branch_types env pind cj (lfj,bty) in - ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, - Array.map j_val lfj); - uj_type = rslty }) + type_case_branches env indspec (make_judge p pt) c in + let () = check_branch_types env pind c ct lft bty in + rslty -let judge_of_projection env p cj = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - let ty = substl (cj.uj_val :: List.rev args) ty in - {uj_val = mkProj (p,cj.uj_val); - uj_type = ty} + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in +let check_fixpoint env lna lar vdef vdeft = + let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try - conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna vdefj lar + error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar (************************************************************************) (************************************************************************) @@ -419,95 +339,96 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> - let cj = execute env c in - judge_of_projection env p cj + let ct = execute env c in + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let jl = execute_array env args in - let j = + let argst = execute_array env args in + let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | Ind ind when Environ.template_polymorphic_pind ind env -> + (* Template sort-polymorphism of inductive types *) + let args = Array.map (fun t -> lazy t) argst in + type_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_pconstant cst env -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* Full or no sort-polymorphism *) + execute env f in - judge_of_apply env j jl + + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let j' = execute env1 c2 in - judge_of_abstraction env name varj j' + let _ = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let c2t = execute env1 c2 in + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let varj' = execute_type env1 c2 in - judge_of_product env name varj varj' + let vars = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let vars' = execute_is_type env1 c2 in + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let j1 = execute env c1 in - let j2 = execute_type env c2 in - let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in - let j' = execute env1 c3 in - judge_of_letin env name j1 j2 j' + let c1t = execute env c1 in + let _c2s = execute_is_type env c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in + let env1 = push_rel (LocalDef (name,c1,c2)) env in + let c3t = execute env1 c3 in + subst1 c1 c3t | Cast (c,k,t) -> - let cj = execute env c in - let tj = execute_type env t in - judge_of_cast env cj k tj + let ct = execute env c in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in + t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> - let cj = execute env c in - let pj = execute env p in - let lfj = execute_array env lf in - judge_of_case env ci pj cj lfj + let ct = execute env c in + let pt = execute env p in + let lft = execute_array env lf in + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; - make_judge (mkFix fix) fix_ty + check_fix env fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty) + check_cofix env cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -516,53 +437,158 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_type env constr = - let j = execute env constr in - type_judgment env j +and execute_is_type env constr = + let t = execute env constr in + check_type env constr t and execute_recdef env (names,lar,vdef) i = - let larj = execute_array env lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lart = execute_array env lar in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 vdef in - let vdefv = Array.map j_val vdefj in - let () = type_fixpoint env1 names lara vdefj in - (lara.(i),(names,lara,vdefv)) + let vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names lara vdef vdeft in + (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let j = execute env constr in - assert (eq_constr j.uj_val constr); - j + let t = execute env constr in + make_judge constr t + +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key (fun b c -> infer b c) + else (fun b c -> infer b c) + +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t -(* let infer_key = Profile.declare_profile "infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } let infer_type env constr = - let j = execute_type env constr in - j + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in - jv + make_judgev cv jv (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDefEntry c -> - let j = infer env c in - LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssumEntry c -> - let j = infer env c in - LocalAssum (Name id, assumption_of_judgment env j) + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +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 cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] l + +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) -> + let ind, l = decompose_app (whd_all env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t + | _ -> + RegularArity t diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2112284ea6..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,24 +98,15 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit - -val type_of_constant : env -> pconstant -> types constrained - val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types @@ -127,4 +115,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.section_context -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d505..4affb5f9fb 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,8 @@ open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -160,14 +161,15 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> @@ -179,6 +181,15 @@ let subst_of_rel_context_instance sign l = let adjust_subst_to_rel_context sign l = List.rev (subst_of_rel_context_instance sign l) +let adjust_rel_to_rel_context sign n = + let rec aux sign = + let open RelDecl in + match sign with + | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) + | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | [] -> (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function diff --git a/kernel/vars.mli b/kernel/vars.mli index 574d50eccb..f7535e6d8f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +(** Take an index in an instance of a context and returns its index wrt to + the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) +val adjust_rel_to_rel_context : Context.Rel.t -> int -> int + (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if |