Correct coqchk reduction

14 files changed, 328 insertions, 27 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 364558755..f9d082ab1 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -323,7 +323,9 @@ type mutual_inductive_body = {
 
     mind_polymorphic : bool; (** Is it polymorphic or not *)
 
-    mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
+    mind_cumulative : bool; (** Is it cumulative or not *)
+
+    mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b8294e795..ac8388f6e 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -328,6 +328,12 @@ let zshift n s =
     | (_,Zshift(k)::s) -> Zshift(n+k)::s
     | _ -> Zshift(n)::s
 
+let rec stack_args_size = function
+  | Zapp v :: s -> Array.length v + stack_args_size s
+  | Zshift(_)::s -> stack_args_size s
+  | Zupdate(_)::s -> stack_args_size s
+  | _ -> 0
+
 (* Lifting. Preserves sharing (useful only for cell with norm=Red).
    lft_fconstr always create a new cell, while lift_fconstr avoids it
    when the lift is 0. *)
diff --git a/checker/closure.mli b/checker/closure.mli
index 8b1f246c2..8da9ad4ea 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -125,6 +125,9 @@ type stack_member =
 and stack = stack_member list
 
 val append_stack : fconstr array -> stack -> stack
+
+val stack_args_size : stack -> int
+    
 val eta_expand_stack : stack -> stack
  
 val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 6c38f38e2..00ff447cc 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -524,6 +524,50 @@ let check_positivity env_ar mind params nrecp inds =
   let wfp = Rtree.mk_rec irecargs in
   Array.iter2 (fun ind wfpi -> check_subtree ind.mind_recargs wfpi) inds wfp
 
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : constr) numparams is_arity =
+  let numchecked = ref 0 in
+  let basic_check ev tp =
+    if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+    numchecked := !numchecked + 1
+  in
+  let check_typ typ typ_env =
+    match typ with
+    | LocalAssum (_, typ') ->
+      begin
+       try
+          basic_check typ_env typ'; Environ.push_rel typ typ_env
+        with NotConvertible -> 
+          anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+      end
+    | _ -> anomaly (Pp.str "")
+  in
+  let typs, codom = dest_prod env arcn in
+  let last_env = fold_rel_context_outside check_typ typs ~init:env in
+  if not is_arity then basic_check last_env codom else ()
+
+(* 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_univs_level_constr sbsubst in
+    let uctx = Univ.UInfoInd.univ_context mib.mind_universes in
+    let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
+    let constraints_other = Univ.subst_univs_level_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 } ->
+      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 _ -> ()
+    ) inds
+
 (************************************************************************)
 (************************************************************************)
 
@@ -547,6 +591,8 @@ let check_inductive env kn mib =
   let env_ar = typecheck_arity env params mib.mind_packets in
   (*  - 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; *)
   (* 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/inductive.ml b/checker/inductive.ml
index f890adba9..30c5f878a 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -56,7 +56,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 
 let inductive_instance mib =
   if mib.mind_polymorphic then
-    UContext.instance mib.mind_universes
+    UContext.instance (UInfoInd.univ_context mib.mind_universes)
   else Instance.empty
 
 (************************************************************************)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index ba0b01784..70c0bdad0 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -117,6 +117,10 @@ let beta_appvect c v =
 (*                         Conversion                               *)
 (********************************************************************)
 
+type conv_pb =
+  | CONV
+  | CUMUL
+
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> unit
 
@@ -152,11 +156,53 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
     cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2)
   else raise NotConvertible
 
-(* Convertibility of sorts *)
+let convert_inductive_instances cv_pb uinfind u u' univs =
+  let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
+  let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+  if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
+          (Univ.Instance.length ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.subst_instance_constraints comp_subst ind_sbcst
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV ->
+        let comp_subst = (Univ.Instance.append u' u) in
+        let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    if (Univ.check_constraints comp_cst univs) then () else raise NotConvertible
+
+let convert_inductives
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  let num_param_arity =
+    mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+  in
+  if not (num_param_arity = sv1 && num_param_arity = sv2) then
+    convert_universes univs u1 u2
+  else
+    let uinfind = mind.mind_universes in
+    convert_inductive_instances cv_pb uinfind u1 u2 univs
+
+let convert_constructors
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  let num_cnstr_args =
+    let nparamsctxt =
+      mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs
+    in
+    nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1)
+  in
+  if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+    convert_universes univs u1 u2
+  else
+    let uinfind = mind.mind_universes in
+    convert_inductive_instances CONV uinfind u1 u2 univs
 
-type conv_pb =
-  | CONV
-  | CUMUL
+(* Convertibility of sorts *)
 
 let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
@@ -375,18 +421,31 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if mind_equiv_infos infos ind1 ind2
-	then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-        else raise NotConvertible
-
-     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	 if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2
-	 then
-	  (let () = convert_universes univ u1 u2 in
-           convert_stacks univ infos lft1 lft2 v1 v2)
-         else raise NotConvertible
+      if mind_equiv_infos infos ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+        let () =
+          if mind.mind_polymorphic && mind.mind_cumulative then
+              convert_inductives cv_pb (mind, snd ind1) u1 (stack_args_size v1)
+                u2 (stack_args_size v2) univ
+          else
+            convert_universes univ u1 u2
+        in
+        convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
+
+    | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+      if Int.equal j1 j2 && mind_equiv_infos infos ind1 ind2 then
+        let mind = Environ.lookup_mind (fst ind1) (infos_env infos) in
+        let () =
+          if mind.mind_polymorphic && mind.mind_cumulative then
+            convert_constructors
+              (mind, snd ind1, j1) u1 (stack_args_size v1)
+              u2 (stack_args_size v2) univ
+          else
+            convert_universes univ u1 u2
+        in
+        convert_stacks univ infos lft1 lft2 v1 v2
+      else raise NotConvertible
 
      (* Eta expansion of records *)
      | (FConstruct ((ind1,j1),u1), _) ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 2d04b77e4..8c10bd6ec 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -97,8 +97,8 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let u = 
     check bool_equal (fun x -> x.mind_polymorphic);
     if mib1.mind_polymorphic then (
-      check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
-      Univ.UContext.instance mib1.mind_universes)
+      check Univ.Instance.equal (fun x -> Univ.UContext.instance (Univ.UInfoInd.univ_context x.mind_universes));
+      Univ.UContext.instance (Univ.UInfoInd.univ_context mib1.mind_universes))
     else Univ.Instance.empty
   in
   let eq_projection_body p1 p2 =
diff --git a/checker/term.ml b/checker/term.ml
index 75c566aeb..f604ac4bd 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -227,6 +227,8 @@ let rel_context_nhyps hyps =
   nhyps 0 hyps
 let fold_rel_context f l ~init = List.fold_right f l init
 
+let fold_rel_context_outside f l ~init = List.fold_right f l init
+
 let map_rel_decl f = function
   | LocalAssum (n, typ) as decl ->
      let typ' = f typ in
@@ -447,3 +449,37 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
+
+let subst_univs_level_constr subst c =
+  if Univ.is_empty_level_subst subst then c
+  else 
+    let f = Univ.Instance.subst_fn (Univ.subst_univs_level_level subst) in
+    let changed = ref false in
+    let rec aux t = 
+      match t with
+      | Const (c, u) -> 
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Const (c, u'))
+      | Ind (i, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+	  let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Ind (i, u'))
+      | Construct (c, u) ->
+	if Univ.Instance.is_empty u then t
+	else 
+          let u' = f u in 
+	    if u' == u then t
+	    else (changed := true; Construct (c, u'))
+      | Sort (Type u) -> 
+         let u' = Univ.subst_univs_level_universe subst u in
+	   if u' == u then t else 
+	     (changed := true; Sort (sort_of_univ u'))
+      | _ -> map_constr aux t
+    in
+    let c' = aux c in
+      if !changed then c' else c
diff --git a/checker/term.mli b/checker/term.mli
index 6b026d056..ccf5b59e0 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -33,6 +33,8 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 val fold_rel_context :
   (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
+val fold_rel_context_outside :
+  (rel_declaration -> 'a -> 'a) -> rel_context -> init:'a -> 'a
 val map_rel_decl : (constr -> constr) -> rel_declaration -> rel_declaration
 val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 val extended_rel_list : int -> rel_context -> constr list
@@ -55,3 +57,4 @@ val eq_constr : constr -> constr -> bool
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Univ.universe_instance -> constr -> constr
 val subst_instance_context : Univ.universe_instance -> rel_context -> rel_context
+val subst_univs_level_constr : Univ.universe_level_subst -> constr -> constr
diff --git a/checker/univ.ml b/checker/univ.ml
index 571743231..fa884d9d0 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1056,7 +1056,9 @@ module Instance : sig
     val subst_fn : universe_level_subst_fn -> t -> t
     val subst : universe_level_subst -> t -> t
     val pr : t -> Pp.std_ppcmds
-    val check_eq : t check_function 
+    val check_eq : t check_function
+    val length : t -> int
+    val append : t -> t -> t
 end = 
 struct
   type t = Level.t array
@@ -1099,6 +1101,7 @@ struct
 	(* [h] must be positive. *)
 	let h = !accu land 0x3FFFFFFF in
 	  h
+
   end
 
   module HInstance = Hashcons.Make(HInstancestruct)
@@ -1135,6 +1138,10 @@ struct
 	   (Int.equal i (Array.length t1)) || (check_eq_level g t1.(i) t2.(i) && aux (i + 1))
 	 in aux 0)
 
+  let length = Array.length
+
+  let append = Array.append
+  
 end
 
 type universe_instance = Instance.t
@@ -1156,6 +1163,44 @@ end
 
 type universe_context = UContext.t
 
+module UInfoInd =
+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_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 universe_info_ind = UInfoInd.t
+
 module ContextSet =
 struct
   type t = LSet.t constrained
@@ -1166,6 +1211,8 @@ struct
 end
 type universe_context_set = ContextSet.t
 
+
+
 (** Substitutions. *)
 
 let is_empty_subst = LMap.is_empty
@@ -1185,6 +1232,22 @@ let subst_univs_level_universe subst u =
     if u == u' then u
     else Universe.sort u'
 
+let subst_univs_level_instance subst i =
+  let i' = Instance.subst_fn (subst_univs_level_level subst) i in
+    if i == i' then i
+    else i'
+
+let subst_univs_level_constraint subst (u,d,v) =
+  let u' = subst_univs_level_level subst u 
+  and v' = subst_univs_level_level subst v in
+    if d != Lt && Level.equal u' v' then None
+    else Some (u',d,v')
+
+let subst_univs_level_constraints subst csts =
+  Constraint.fold 
+    (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
+    csts Constraint.empty 
+
 (** Substitute instance inst for ctx in csts *)
 
 let subst_instance_level s l =
diff --git a/checker/univ.mli b/checker/univ.mli
index 7d4c629ab..edf828dae 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -71,6 +71,8 @@ type 'a check_function = universes -> 'a -> 'a -> bool
 val check_leq : universe check_function
 val check_eq : universe check_function
 
+
+
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
 
@@ -170,6 +172,12 @@ sig
 
   val check_eq : t check_function
   (** Check equality of instances w.r.t. a universe graph *)
+
+  val length : t -> int
+  (** Compute the length of the instance  *)
+
+  val append : t -> t -> t
+  (** Append two universe instances *)
 end
 
 type universe_instance = Instance.t
@@ -190,6 +198,27 @@ sig
 
 end
 
+type universe_context = UContext.t
+
+module UInfoInd :
+sig
+  type t
+
+  val make : universe_context * universe_context -> t
+
+  val empty : t
+
+  val univ_context : t -> universe_context
+  val subtyp_context : t -> universe_context
+
+  val from_universe_context : universe_context -> universe_instance -> t
+
+  val subtyping_susbst : t -> universe_level_subst
+
+end
+
+type universe_info_ind = UInfoInd.t
+
 module ContextSet :
   sig 
     type t
@@ -198,7 +227,6 @@ module ContextSet :
     val constraints : t -> constraints
   end
 
-type universe_context = UContext.t
 type universe_context_set = ContextSet.t
 
 val merge_context : bool -> universe_context -> universes -> universes
@@ -210,6 +238,8 @@ val is_empty_level_subst : universe_level_subst -> bool
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
+val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
+val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
 (** Level to universe substitutions. *)
 
diff --git a/checker/values.ml b/checker/values.ml
index c175aed68..c58f56a9b 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6466d8cc443b5896cb905776df0cc49e  checker/cic.mli
+MD5 6153d4f8fb414a8f14797636ab10f55e  checker/cic.mli
 
 *)
 
@@ -272,7 +272,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     v_rctxt;
     v_bool;
-    v_context;
+    v_bool;
+    v_tuple "universes" [|v_context; v_context|];
     Opt v_bool;
     v_typing_flags|]
 
diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
new file mode 100644
index 000000000..5d245aaa5
--- /dev/null
+++ b/test-suite/coqchk/cumulativity.v
@@ -0,0 +1,52 @@
+Set Universe Polymorphism.
+Set Ind Cumulativity.
+Set Printing Universes.
+
+Inductive List (A: Type) := nil | cons : A -> List A -> List A.
+
+Section ListLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftL {A} : List@{i} A -> List@{j} A := fun x => x.
+
+End ListLift.
+
+Lemma LiftL_Lem A (l : List A) : l = LiftL l.
+Proof. reflexivity. Qed.
+
+Section ListLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LowerL {A : Type@{i}} : List@{j} A -> List@{i} A := fun x => x.
+
+End ListLower.
+
+Lemma LowerL_Lem@{i j} (A : Type@{j}) (l : List@{i} A) : l = LowerL l.
+Proof. reflexivity. Qed.
+
+Inductive Tp := tp : Type -> Tp.
+
+Section TpLift.
+  Universe i j.
+
+  Constraint i < j.
+
+  Definition LiftTp : Tp@{i} -> Tp@{j} := fun x => x.
+
+End TpLift.
+
+Lemma LiftC_Lem (t : Tp) : LiftTp t = t.
+Proof. reflexivity. Qed.
+
+Section TpLower.
+  Universe i j.
+
+  Constraint i < j.
+
+  Fail Definition LowerTp : Tp@{j} -> Tp@{i} := fun x => x.
+
+End TpLower.
\ No newline at end of file
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f130708c4..580c81a0b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1368,9 +1368,9 @@ let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "inductive cumulativity";
-      optkey   = ["Inductive"; "Cumulativity"];
-      optread  = Flags.is_universe_polymorphism;
-      optwrite = Flags.make_universe_polymorphism }
+      optkey   = ["Ind"; "Cumulativity"];
+      optread  = Flags.is_inductive_cumulativity;
+      optwrite = Flags.make_inductive_cumulativity }
 
 let _ =
   declare_int_option