diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 4 | ||||
| -rw-r--r-- | checker/declarations.ml | 8 | ||||
| -rw-r--r-- | checker/environ.ml | 8 | ||||
| -rw-r--r-- | checker/environ.mli | 2 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 14 | ||||
| -rw-r--r-- | checker/subtyping.ml | 4 | ||||
| -rw-r--r-- | checker/typeops.ml | 25 | ||||
| -rw-r--r-- | checker/typeops.mli | 3 | ||||
| -rw-r--r-- | checker/values.ml | 7 |
9 files changed, 15 insertions, 60 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 14fa7c774..59dd5bc4d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -182,8 +182,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (constr, rel_context * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -226,7 +224,7 @@ type typing_flags = { type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; const_proj : projection_body option; diff --git a/checker/declarations.ml b/checker/declarations.ml index 2eefe4781..093d999a3 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -515,12 +515,6 @@ let subst_rel_declaration sub = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - -let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s - let constant_is_polymorphic cb = match cb.const_universes with | Monomorphic_const _ -> false @@ -531,7 +525,7 @@ let constant_is_polymorphic cb = let subst_const_body sub cb = { cb with const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type } + const_type = subst_mps sub cb.const_type } let subst_regular_ind_arity sub s = diff --git a/checker/environ.ml b/checker/environ.ml index d3f393c65..a0818012c 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -124,12 +124,6 @@ let constraints_of cb u = | Monomorphic_const _ -> Univ.Constraint.empty | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in @@ -137,7 +131,7 @@ let constant_type env (kn,u) = | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty | Polymorphic_const ctx -> let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + (subst_instance_constr u cb.const_type, csts) exception NotEvaluableConst of const_evaluation_result diff --git a/checker/environ.mli b/checker/environ.mli index 754c295d2..8e8d0fd49 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -46,7 +46,7 @@ val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constant_type Univ.constrained +val constant_type : env -> constant puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4948f6008..b6816dd48 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -35,15 +35,11 @@ let check_constant_declaration env kn cb = push_context ~strict:false ctx env in let envty, ty = - match cb.const_type with - RegularArity ty -> - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in envty, ty - | TemplateArity(ctxt,par) -> - let _ = check_ctxt env' ctxt in - check_polymorphic_arity env' ctxt par; - env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + let ty = cb.const_type in + let ty', cu = refresh_arity ty in + let envty = push_context_set cu env' in + let _ = infer_type envty ty' in + envty, ty in let () = match body_of_constant cb with diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 3097c3a0b..68a467bea 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -294,8 +294,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in (*Start by checking types*) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let typ1 = cb1.const_type in + let typ2 = cb2.const_type in check_type env typ1 typ2; (* Now we check the bodies: - A transparent constant can only be implemented by a compatible diff --git a/checker/typeops.ml b/checker/typeops.ml index f2cbfec7d..9f39d588a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -69,35 +69,16 @@ let judge_of_relative env n = (* Type of constants *) - -let type_of_constant_type_knowing_parameters 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_type_knowing_parameters env ty paramtyps, cu - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = +let judge_of_constant env (kn,u as cst) = let _cb = try lookup_constant kn env with Not_found -> failwith ("Cannot find constant: "^Constant.to_string kn) in - let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - (* Type of an application. *) let judge_of_apply env (f,funj) argjv = @@ -276,8 +257,6 @@ let rec execute env cstr = match f with | Ind ind -> judge_of_inductive_knowing_parameters env ind jl - | Const cst -> - judge_of_constant_knowing_parameters env cst jl | _ -> (* No template polymorphism *) execute env f diff --git a/checker/typeops.mli b/checker/typeops.mli index 2be461b05..d9f2915a3 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -18,6 +18,3 @@ val infer_type : env -> constr -> sorts val check_ctxt : env -> rel_context -> env val check_polymorphic_arity : env -> rel_context -> template_arity -> unit - -val type_of_constant_type : env -> constant_type -> constr - diff --git a/checker/values.ml b/checker/values.ml index e13430e98..c95c3f1b2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 67309b04a86b247431fd3e580ecbb50d checker/cic.mli +MD5 c802f941f368bedd96e931cda0559d67 checker/cic.mli *) @@ -201,9 +201,6 @@ let v_engagement = v_impredicative_set let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] -let v_cst_type = - v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|] - let v_cst_def = v_sum "constant_def" 0 [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] @@ -222,7 +219,7 @@ let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_contex let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; - v_cst_type; + v_constr; Any; v_const_univs; Opt v_projbody; |