Enable the checking of ind subtyping in checker

3 files changed, 61 insertions, 22 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 69dd6f57a..cac7e6313 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -549,25 +549,24 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : con
 (* Check that the subtyping information inferred for inductive types in the block is correct. *)
 (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
 let check_subtyping mib paramsctxt env_ar inds =
-    let numparams = rel_context_nhyps paramsctxt in
-    let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
-    let dosubst = subst_instance_constr sbsubst in
-    let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
-    let instance_other = Univ.subst_instance_instance sbsubst (Univ.UContext.instance uctx) in
-    let constraints_other = Univ.subst_instance_constraints sbsubst (Univ.UContext.constraints uctx) in
-    let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
-    let env' = Environ.push_context uctx env_ar in
-    let env'' = Environ.push_context uctx_other env' in
-    let envsb = push_context (Univ.UInfoInd.subtyp_context mib.mind_universes) env'' in
-    (* process individual inductive types: *)
-    Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
+  let numparams = rel_context_nhyps paramsctxt in
+  let sbsubst = Univ.UInfoInd.subtyping_susbst mib.mind_universes in
+  let other_instnace = Univ.UInfoInd.subtyping_other_instance mib.mind_universes in
+  let dosubst = subst_univs_level_constr sbsubst in
+  let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
+  let uctx_other = Univ.UContext.make (other_instnace, Univ.UContext.constraints uctx) in
+  let env = Environ.push_context uctx env_ar in
+  let env = Environ.push_context uctx_other env in
+  let env = Environ.push_context (Univ.instantiate_univ_context (Univ.UInfoInd.subtyp_context mib.mind_universes)) env in
+  (* process individual inductive types: *)
+  Array.iter (fun { mind_user_lc = lc; mind_arity = arity } ->
       match arity with
-        | RegularArity { mind_user_arity = full_arity} ->
-           check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
-           Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
-        | TemplateArity _ -> ()
+      | RegularArity { mind_user_arity = full_arity} ->
+        check_subtyping_arity_constructor env dosubst full_arity numparams true;
+        Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+      | TemplateArity _ -> ()
     ) inds
-
+    
 (************************************************************************)
 (************************************************************************)
 
@@ -592,7 +591,8 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
-  (* check_subtyping mib params env_ar mib.mind_packets; *)
+  if mib.mind_cumulative then
+    check_subtyping mib params env_ar mib.mind_packets;
   (* check mind_nparams_rec: positivity condition *)
   check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
diff --git a/checker/univ.ml b/checker/univ.ml
index 525f535e9..92b6a9e86 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -968,7 +968,23 @@ struct
       else Level.compare v v'
 end
 
-module Constraint = Set.Make(UConstraintOrd)
+let pr_constraint_type op = 
+  let op_str = match op with
+    | Lt -> " < "
+    | Le -> " <= "
+    | Eq -> " = "
+  in str op_str
+
+module Constraint = 
+struct 
+  module S = Set.Make(UConstraintOrd)
+  include S
+
+  let pr prl c =
+    fold (fun (u1,op,u2) pp_std ->
+      pp_std ++ prl u1 ++ pr_constraint_type op ++
+	prl u2 ++ fnl () )  c (str "")
+end
 
 let empty_constraint = Constraint.empty
 let merge_constraints c g =
@@ -1159,6 +1175,11 @@ struct
   let make x = x
   let instance (univs, cst) = univs
   let constraints (univs, cst) = cst
+
+  let is_empty (univs, cst) = Instance.is_empty univs && Constraint.is_empty cst
+  let pr prl (univs, cst as ctx) =
+    if is_empty ctx then mt() else
+      h 0 (Instance.pr univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 end
 
 type universe_context = UContext.t
@@ -1193,8 +1214,12 @@ struct
     (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') = (halve_context (UContext.instance subtypcst)) in ctx'
+    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
 
@@ -1308,6 +1333,10 @@ let merge_context_set strict ctx g =
 
 (** Pretty-printing *)
 
+let pr_constraints prl = Constraint.pr prl
+    
+let pr_universe_context = UContext.pr
+
 let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
diff --git a/checker/univ.mli b/checker/univ.mli
index 2bc2653e0..018f8aee2 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -18,6 +18,9 @@ sig
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
+  val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
+  
   val equal : t -> t -> bool
 end
 
@@ -195,7 +198,8 @@ sig
   val make : universe_instance constrained -> t
   val instance : t -> Instance.t
   val constraints : t -> constraints
-
+  val is_empty : t -> bool
+    
 end
 
 type universe_context = UContext.t
@@ -213,7 +217,9 @@ sig
 
   val from_universe_context : universe_context -> universe_instance -> t
 
-  val subtyping_susbst : t -> universe_instance
+  val subtyping_other_instance : t -> universe_instance
+  
+  val subtyping_susbst : t -> universe_level_subst
 
 end
 
@@ -263,4 +269,8 @@ val make_abstract_instance : universe_context -> universe_instance
 									    
 (** {6 Pretty-printing of universes. } *)
 
+val pr_constraint_type : constraint_type -> Pp.std_ppcmds
+val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
+val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
+
 val pr_universes : universes -> Pp.std_ppcmds