diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-07 16:33:47 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-11 14:50:47 +0200 |
commit | 0d9a91113c4112eece0680e433f435fdfb39ea4b (patch) | |
tree | cf90d290a92c02a2297b3a13b77190db9aa4db70 /checker | |
parent | b5ad6a80107f196fa8ffcc4f5dff58bea8c4f70e (diff) |
Getting rid of simple calls to AUContext.instance.
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
Diffstat (limited to 'checker')
-rw-r--r-- | checker/inductive.ml | 7 | ||||
-rw-r--r-- | checker/inductive.mli | 2 | ||||
-rw-r--r-- | checker/reduction.ml | 8 | ||||
-rw-r--r-- | checker/subtyping.ml | 20 | ||||
-rw-r--r-- | checker/univ.ml | 1 | ||||
-rw-r--r-- | checker/univ.mli | 1 |
6 files changed, 11 insertions, 28 deletions
diff --git a/checker/inductive.ml b/checker/inductive.ml index 93ffa329a..a145165aa 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -66,13 +66,6 @@ let inductive_is_cumulative mib = | Polymorphic_ind ctx -> false | Cumulative_ind cumi -> true -let inductive_polymorphic_instance mib = - match mib.mind_universes with - | Monomorphic_ind _ -> Univ.Instance.empty - | Polymorphic_ind ctx -> Univ.AUContext.instance ctx - | Cumulative_ind cumi -> - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) - let inductive_polymorphic_context mib = match mib.mind_universes with | Monomorphic_ind _ -> Univ.UContext.empty diff --git a/checker/inductive.mli b/checker/inductive.mli index 698b8b77c..b8cbda7cf 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -26,8 +26,6 @@ val inductive_is_polymorphic : mutual_inductive_body -> bool val inductive_is_cumulative : mutual_inductive_body -> bool -val inductive_polymorphic_instance : mutual_inductive_body -> Univ.universe_instance - val inductive_polymorphic_context : mutual_inductive_body -> Univ.universe_context val type_of_inductive : env -> mind_specif puniverses -> constr diff --git a/checker/reduction.ml b/checker/reduction.ml index 93b8b907c..0b605820d 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -157,11 +157,11 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = else raise NotConvertible let convert_inductive_instances cv_pb cumi u u' univs = - let ind_instance = - Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi) in + let len_instance = + Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) in let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && - (Univ.Instance.length ind_instance = Univ.Instance.length u')) then + if not ((len_instance = Univ.Instance.length u) && + (len_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else let comp_cst = diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5fd5510a7..303b18476 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -309,27 +309,17 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (CErrors.user_err (Pp.str ( + CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ - "name."))); - if constant_has_body cb2 then error () ; - let u = inductive_polymorphic_instance mind1 in - let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv conv_leq env arity1 typ2 - | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (CErrors.user_err (Pp.str ( + "name.")) + | IndConstr (((kn,i),j),mind1) -> + CErrors.user_err (Pp.str ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ - "name."))); - if constant_has_body cb2 then error () ; - let u1 = inductive_polymorphic_instance mind1 in - let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in - let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv conv env ty1 ty2 + "name.")) let rec check_modules env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in diff --git a/checker/univ.ml b/checker/univ.ml index b434db129..4eebcb25b 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1175,6 +1175,7 @@ struct let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst + let size (univs, _) = Instance.length univs let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst let pr prl (univs, cst as ctx) = diff --git a/checker/univ.mli b/checker/univ.mli index 457ccbdff..faa682cbf 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -209,6 +209,7 @@ sig type t val instance : t -> Instance.t + val size : t -> int end |