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/mod_checking.ml | 37 +++++++++++++++++++------------------
 1 file changed, 19 insertions(+), 18 deletions(-)

(limited to 'checker/mod_checking.ml')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 53316a2cb..12a97bf68 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -14,30 +14,31 @@ open Environ
 
 (** {6 Checking constants } *)
 
-(* let refresh_arity ar = *)
-(*   let ctxt, hd = decompose_prod_assum ar in *)
-(*   match hd with *)
-(*       Sort (Type u) when not (Univ.is_univ_variable u) -> *)
-(*         let u' = Univ.fresh_local_univ() in *)
-(*         mkArity (ctxt,Type u'), *)
-(*         Univ.enforce_leq u u' Univ.empty_constraint *)
-(*     | _ -> ar, Univ.empty_constraint *)
+let refresh_arity ar =
+  let ctxt, hd = decompose_prod_assum ar in
+  match hd with
+      Sort (Type u) when not (Univ.is_univ_variable u) ->
+        let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in
+        mkArity (ctxt,Prop Null), 
+	  Univ.enforce_leq u u' Univ.empty_constraint
+    | _ -> ar, Univ.empty_constraint
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose ppnl (str "  checking cst: " ++ prcon kn);
-(*  let env = add_constraints cb.const_constraints env in*)
+  let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in
   (match cb.const_type with
-      ty ->
-        let env' = add_constraints cb.const_constraints env in (*MS: FIXME*)
-	let _ = infer_type env' ty in
-          (match body_of_constant cb with
+      RegularArity ty ->
+        let ty, cu = refresh_arity ty in
+        let envty = add_constraints cu env in
+        let _ = infer_type envty ty in
+        (match body_of_constant cb with
           | Some bd ->
-              let j = infer env' bd in
-              conv_leq env' j ty
+              let j = infer envty bd in
+              conv_leq envty j ty
           | None -> ())
-    (* | PolymorphicArity(ctxt,par) -> *)
-    (*     let _ = check_ctxt env ctxt in *)
-    (*     check_polymorphic_arity env ctxt par *));
+    | TemplateArity(ctxt,par) ->
+        let _ = check_ctxt env ctxt in
+        check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
 
-- 
cgit v1.2.3