From f912004bbe2c8f77de09cc290c3c687dc4ebf7f8 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Thu, 8 May 2014 13:43:26 +0200
Subject: Adapt the checker to polymorphic universes and projections
 (untested).

---
 checker/cic.mli | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 51 insertions(+), 7 deletions(-)

(limited to 'checker/cic.mli')

diff --git a/checker/cic.mli b/checker/cic.mli
index d2f785abf..484d64973 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -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,11 +188,24 @@ 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;
@@ -185,6 +213,9 @@ type constant_body = {
     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,6 +227,13 @@ 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 } *)
 
@@ -203,7 +241,7 @@ type one_inductive_body = {
 
     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 } *)
 
-- 
cgit v1.2.3