diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 13:43:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-08 19:23:51 +0200 |
| commit | f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 (patch) | |
| tree | eadad13bfd7e178d782bb46a9bd3e0daff84264b /checker/inductive.mli | |
| parent | 0db1d850b940a5f2351c1ec6e26d1f8087064d40 (diff) | |
Adapt the checker to polymorphic universes and projections (untested).
Diffstat (limited to 'checker/inductive.mli')
| -rw-r--r-- | checker/inductive.mli | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/checker/inductive.mli b/checker/inductive.mli index 082bdae19..e223af0c9 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -14,7 +14,7 @@ open Environ (*s Extracting an inductive type from a construction *) -val find_rectype : env -> constr -> inductive * constr list +val find_rectype : env -> constr -> pinductive * constr list type mind_specif = mutual_inductive_body * one_inductive_body @@ -22,12 +22,15 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val type_of_inductive : env -> mind_specif -> constr +val make_inductive_subst : mutual_inductive_body -> Univ.universe_instance -> Univ.universe_subst +val inductive_instance : mutual_inductive_body -> Univ.universe_instance + +val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) -val type_of_constructor : constructor -> mind_specif -> constr +val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive -> mind_specif -> constr array +val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: @@ -36,7 +39,7 @@ val arities_of_specif : mutual_inductive -> mind_specif -> constr array introduced by products) and the type for the whole expression. *) val type_case_branches : - env -> inductive * constr list -> constr * constr -> constr + env -> pinductive * constr list -> constr * constr -> constr -> constr array * constr (* Check a [case_info] actually correspond to a Case expression on the @@ -50,12 +53,12 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) val type_of_inductive_knowing_parameters : - env -> one_inductive_body -> constr array -> constr + env -> mind_specif puniverses -> constr array -> constr val max_inductive_sort : sorts array -> Univ.universe -(* val instantiate_universes : env -> rel_context -> *) -(* inductive_arity -> constr array -> rel_context * sorts *) +val instantiate_universes : env -> rel_context -> + template_arity -> constr array -> rel_context * sorts (***************************************************************) (* Debug *) |