Correct coqchk reduction

1 files changed, 75 insertions, 16 deletions

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), _) ->