Fix checker/values.ml with latest changes due to projections and universes.

1 files changed, 35 insertions, 16 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 9d2444309a..b38744cc7e 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -93,10 +93,14 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
 
 (** kernel/univ *)
 
-let v_level = v_sum "level" 1 [|[|Int;v_dp|]|]
-let v_univ = v_sum "univ" 0
-  [|[|v_level|];
-    [|List v_level;List v_level|]|]
+let v_raw_level = v_sum "raw_level" 2 (* Prop, Set *) 
+  [|(*Level*)[|Int;v_dp|]; (*Var*)[|Int|]|]
+let v_level = v_tuple "level" [|Int;v_raw_level|] 
+let v_expr = v_tuple "levelexpr" [|v_level;Int|]
+let v_univ = 
+  let rec vuniv = 
+    Tuple("hconsnode", [|Int;Int; Sum ("univ", 1, [|(*Cons*)[|v_expr;vuniv|]|])|])
+  in vuniv
 
 let v_cstrs =
   Annot
@@ -105,20 +109,22 @@ let v_cstrs =
        (v_tuple "univ_constraint"
           [|v_level;v_enum "order_request" 3;v_level|]))
 
+let v_instance = Annot ("instance", Array v_level)
+let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|]
 
 (** kernel/term *)
 
 let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|]
 let v_sortfam = v_enum "sorts_family" 3
 
+let v_puniverses v = v_tuple "punivs" [|v;v_instance|]
+
 let v_caseinfo =
   let v_cstyle = v_enum "case_style" 5 in
   let v_cprint = v_tuple "case_printing" [|Int;v_cstyle|] in
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
-let v_cast = v_enum "cast_kind" 3
-(** NB : In fact there are 4 cast markers, but the last one
-   (REVERTcast) isn't supposed to appear in a vo *)
+let v_cast = v_enum "cast_kind" 4
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -132,12 +138,13 @@ let rec v_constr =
     [|v_name;v_constr;v_constr|]; (* Lambda *)
     [|v_name;v_constr;v_constr;v_constr|]; (* LetIn *)
     [|v_constr;Array v_constr|]; (* App *)
-    [|v_cst|]; (* Const *)
-    [|v_ind|]; (* Ind *)
-    [|v_cons|]; (* Construct *)
+    [|v_puniverses v_cst|]; (* Const *)
+    [|v_puniverses v_ind|]; (* Ind *)
+    [|v_puniverses v_cons|]; (* Construct *)
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
-    [|v_cofix|] (* CoFix *)
+    [|v_cofix|]; (* CoFix *)
+    [|v_cst;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -187,7 +194,7 @@ let v_lazy_constr =
 let v_engagement = v_enum "eng" 1
 
 let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_univ);v_univ|]
+  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
 
 let v_cst_type =
   v_sum "constant_type" 0 [|[|v_constr|];[|v_rctxt;v_pol_arity|]|]
@@ -196,12 +203,18 @@ let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
+let v_projbody =
+  v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
+			      v_constr|]
+
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_cst_type;
     Any;
-    v_cstrs;
+    v_bool;
+    v_context;
+    Opt v_projbody;
     v_bool|]
 
 let v_recarg = v_sum "recarg" 1 (* Norec *)
@@ -236,16 +249,22 @@ let v_one_ind = v_tuple "one_inductive_body"
     Int;
     Any|]
 
+let v_finite = v_enum "recursivity_kind" 3
+let v_mind_record = Annot ("mind_record", 
+			   Opt (v_tuple "record" [| Array v_cst; Array v_projbody |]))
+
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
-    v_bool;
-    v_bool;
+    v_mind_record;
+    v_finite;
     Int;
     v_section_ctxt;
     Int;
     Int;
     v_rctxt;
-    v_cstrs|]
+    v_bool;
+    v_context;
+    Opt v_bool|]
 
 let v_with =
   Sum ("with_declaration_body",0,