From e2e41c94f1f965e8c7d8bd4a93b58774821c2273 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 18 Jul 2017 22:55:28 +0200
Subject: Fixing the checker w.r.t. wrongly used abstract universe contexts.

It seems we were not testing the checker on cumulative inductive types,
because judging from the code, it would just have exploded in anomalies.
Before this patch, the checker was mixing De Bruijn indices with named
variables, resulting in ill-formed universe contexts used throughout the
checking of cumulative inductive types.

This patch also gets rid of a lot of now dead code, and removes abstraction
breaking code from the checker.
---
 checker/univ.ml | 44 ++++----------------------------------------
 1 file changed, 4 insertions(+), 40 deletions(-)

(limited to 'checker/univ.ml')

diff --git a/checker/univ.ml b/checker/univ.ml
index 2cd4252b2..e3abc436f 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1075,6 +1075,7 @@ module Instance : sig
     val check_eq : t check_function
     val length : t -> int
     val append : t -> t -> t
+    val of_array : Level.t array -> t
 end = 
 struct
   type t = Level.t array
@@ -1157,7 +1158,9 @@ struct
   let length = Array.length
 
   let append = Array.append
-  
+
+  let of_array i = i
+
 end
 
 (** Substitute instance inst for ctx in csts *)
@@ -1231,43 +1234,11 @@ module CumulativityInfo =
 struct
   type t = universe_context * universe_context
 
-  let make x =
-    if (Array.length (UContext.instance (snd x))) =
-       (Array.length (UContext.instance (fst x))) * 2 then x
-    else anomaly (Pp.str "Invalid subtyping information encountered!")
-
-  let empty = (UContext.empty, UContext.empty)
-
-  let halve_context ctx =
-    let len = Array.length ctx in
-    let halflen = len / 2 in
-    ((Array.sub ctx 0 halflen), (Array.sub ctx halflen halflen))
-
   let univ_context (univcst, subtypcst) = univcst
   let subtyp_context (univcst, subtypcst) = subtypcst
 
-  let create_trivial_subtyping ctx ctx' =
-    CArray.fold_left_i
-      (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
-      Constraint.empty ctx
-
-  let from_universe_context univcst freshunivs =
-    let inst = (UContext.instance univcst) in
-    assert (Array.length freshunivs = Array.length inst);
-    (univcst, UContext.make (Array.append inst freshunivs,
-                             create_trivial_subtyping inst freshunivs))
-
-  let subtyping_other_instance (univcst, subtypcst) =
-    let (_, ctx') = (halve_context (UContext.instance subtypcst)) in ctx'
-  
-  let subtyping_susbst (univcst, subtypcst) =
-    let (ctx, ctx') = (halve_context (UContext.instance subtypcst)) in
-    Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
-
 end
 
-type cumulativity_info = CumulativityInfo.t
-
 module ACumulativityInfo = CumulativityInfo
 type abstract_cumulativity_info = ACumulativityInfo.t
 
@@ -1315,13 +1286,6 @@ let subst_univs_level_universe subst u =
 let make_abstract_instance (ctx, _) = 
   Array.mapi (fun i l -> Level.var i) ctx
 
-(** Substitute instance inst for ctx in csts *)
-let instantiate_univ_context (ctx, csts) = 
-  (ctx, subst_instance_constraints ctx csts)
-
-let instantiate_cumulativity_info (ctx, ctx') = 
-  (instantiate_univ_context ctx, instantiate_univ_context ctx')
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
-- 
cgit v1.2.3