Permalink
Browse files

Adapt the checker to polymorphic universes and projections (untested).

  • Loading branch information...
1 parent 0db1d85 commit f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 @mattam82 mattam82 committed May 8, 2014
View
@@ -297,7 +297,8 @@ let rec explain_exn = function
str("\nCantApplyBadType at argument " ^ string_of_int n)
| CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
| IllFormedRecBody _ -> str"IllFormedRecBody"
- | IllTypedRecBody _ -> str"IllTypedRecBody"))
+ | IllTypedRecBody _ -> str"IllTypedRecBody"
+ | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"))
| Indtypes.InductiveError e ->
hov 0 (str "Error related to inductive types")
View
@@ -79,6 +79,10 @@ type 'constr pfixpoint =
(int array * int) * 'constr prec_declaration
type 'constr pcofixpoint =
int * 'constr prec_declaration
+type 'a puniverses = 'a Univ.puniverses
+type pconstant = constant puniverses
+type pinductive = inductive puniverses
+type pconstructor = constructor puniverses
type constr =
| Rel of int
@@ -91,12 +95,13 @@ type constr =
| Lambda of Name.t * constr * constr
| LetIn of Name.t * constr * constr * constr
| App of constr * constr array
- | Const of constant
- | Ind of inductive
- | Construct of constructor
+ | Const of pconstant
+ | Ind of pinductive
+ | Construct of pconstructor
| Case of case_info * constr * constr * constr array
| Fix of constr pfixpoint
| CoFix of constr pcofixpoint
+ | Proj of constant * constr
type existential = constr pexistential
type rec_declaration = constr prec_declaration
@@ -163,7 +168,17 @@ type engagement = ImpredicativeSet
(** {6 Representation of constants (Definition/Axiom) } *)
-type constant_type = constr
+
+type template_arity = {
+ template_param_levels : Univ.universe option list;
+ template_level : Univ.universe;
+}
+
+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. *)
@@ -173,18 +188,34 @@ type inline = int option
(** A constant can have no body (axiom/parameter), or a
transparent body, or an opaque one *)
+(** Projections are a particular kind of constant:
+ always transparent. *)
+
+type projection_body = {
+ proj_ind : mutual_inductive;
+ proj_npars : int;
+ proj_arg : int;
+ proj_type : constr; (* Type under params *)
+ proj_body : constr; (* For compatibility, the match version *)
+}
+
type constant_def =
| Undef of inline
| Def of constr_substituted
| OpaqueDef of lazy_constr
+type constant_universes = Univ.universe_context
+
type constant_body = {
const_hyps : section_context; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : to_patch_substituted;
const_constraints : Univ.constraints;
const_native_name : native_name ref;
+ const_polymorphic : bool; (** Is it polymorphic or not *)
+ const_universes : constant_universes;
+ const_proj : projection_body option;
const_inline_code : bool }
(** {6 Representation of mutual inductive types } *)
@@ -196,14 +227,21 @@ type recarg =
type wf_paths = recarg Rtree.t
+type regular_inductive_arity = {
+ mind_user_arity : constr;
+ mind_sort : sorts;
+}
+
+type inductive_arity = (regular_inductive_arity, template_arity) declaration_arity
+
type one_inductive_body = {
(** {8 Primitive datas } *)
mind_typename : Id.t; (** Name of the type: [Ii] *)
mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
- mind_arity : constr; (** Arity sort and original user arity if monomorphic *)
+ mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
@@ -245,7 +283,9 @@ type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
- mind_record : bool; (** Whether the inductive type has been declared as a record *)
+ mind_record : (constr * constant array) option;
+ (** Whether the inductive type has been declared as a record,
+ In that case we get its canonical eta-expansion and list of projections. *)
mind_finite : bool; (** Whether the type is inductive or coinductive *)
@@ -259,7 +299,11 @@ type mutual_inductive_body = {
mind_params_ctxt : rel_context; (** The context of parameters (includes let-in declaration) *)
- mind_constraints : Univ.constraints; (** Universes constraints enforced by the inductive declaration *)
+ mind_polymorphic : bool; (** Is it polymorphic or not *)
+
+ mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+
+ mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
(** {8 Data for native compilation } *)
Oops, something went wrong.

0 comments on commit f912004

Please sign in to comment.