Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.

1 files changed, 120 insertions, 37 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index cf40263f61..1e39756d47 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -56,7 +56,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
     | (Zproj _p1::s1, Zproj _p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-    | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) ->
+    | (ZcaseT(_c1,_,_,_,_,_)::s1, ZcaseT(_c2,_,_,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -74,7 +74,7 @@ type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
   | Zlproj of Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
-  | Zlcase of case_info * lift * constr * constr array * fconstr subs
+  | Zlcase of case_info * lift * Univ.Instance.t * constr array * case_return * case_branch array * fconstr subs
   | Zlprimitive of
      CPrimitives.t * pconstant * lft_fconstr list * lft_fconstr next_native_args
 and lft_constr_stack = lft_constr_stack_elt list
@@ -109,8 +109,8 @@ let pure_stack lfts stk =
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
-            | (ZcaseT(ci,p,br,e),(l,pstk)) ->
-                (l,Zlcase(ci,l,p,br,e)::pstk)
+            | (ZcaseT(ci,u,pms,p,br,e),(l,pstk)) ->
+                (l,Zlcase(ci,l,u,pms,p,br,e)::pstk)
             | (Zprimitive(op,c,rargs,kargs),(l,pstk)) ->
                 (l,Zlprimitive(op,c,List.map (fun t -> (l,t)) rargs,
                             List.map (fun (k,t) -> (k,(l,t))) kargs)::pstk))
@@ -233,6 +233,9 @@ let convert_instances ~flex u u' (s, check) =
 
 exception MustExpand
 
+let convert_instances_cumul pb var u u' (s, check) =
+  (check.compare_cumul_instances pb var u u' s, check)
+
 let get_cumulativity_constraints cv_pb variance u u' =
   match cv_pb with
   | CONV ->
@@ -294,8 +297,6 @@ let conv_table_key infos ~nargs k1 k2 cuniv =
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
 
-exception IrregularPatternShape
-
 let unfold_ref_with_args infos tab fl v =
   match unfold_reference infos tab fl with
   | Def def -> Some (def, v)
@@ -327,17 +328,6 @@ let push_relevance infos r =
 let push_relevances infos nas =
   { infos with cnv_inf = CClosure.push_relevances infos.cnv_inf nas }
 
-let rec skip_pattern infos relevances n c1 c2 =
-  if Int.equal n 0 then {infos with cnv_inf = CClosure.set_info_relevances infos.cnv_inf relevances}, c1, c2
-  else match kind c1, kind c2 with
-    | Lambda (x, _, c1), Lambda (_, _, c2) ->
-      skip_pattern infos (Range.cons x.Context.binder_relevance relevances) (pred n) c1 c2
-    | _ -> raise IrregularPatternShape
-
-let skip_pattern infos n c1 c2 =
-  if Int.equal n 0 then infos, c1, c2
-  else skip_pattern infos (info_relevances infos.cnv_inf) n c1 c2
-
 let is_irrelevant infos lft c =
   let env = info_env infos.cnv_inf in
   try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
@@ -364,6 +354,39 @@ let eta_expand_constructor env ((ind,ctor),u as pctor) =
   let c = Term.it_mkLambda_or_LetIn c ctx in
   inject c
 
+let inductive_subst (mind, _) mib u pms =
+  let open Context.Rel.Declaration in
+  let ntypes = mib.mind_ntypes in
+  let rec self i accu =
+    if Int.equal i ntypes then accu
+    else self (i + 1) (subs_cons (inject (mkIndU ((mind, i), u))) accu)
+  in
+  let accu = self 0 (subs_id 0) in
+  let rec mk_pms pms ctx = match ctx, pms with
+  | [], [] -> accu
+  | LocalAssum _ :: ctx, c :: pms ->
+    let subs = mk_pms pms ctx in
+    subs_cons c subs
+  | LocalDef (_, c, _) :: ctx, pms ->
+    let c = Vars.subst_instance_constr u c in
+    let subs = mk_pms pms ctx in
+    subs_cons (mk_clos subs c) subs
+  | LocalAssum _ :: _, [] | [], _ :: _ -> assert false
+  in
+  mk_pms (List.rev pms) mib.mind_params_ctxt
+
+let esubst_of_rel_context_instance ctx u args e =
+  let open Context.Rel.Declaration in
+  let rec aux lft e args ctx = match ctx with
+  | [] -> lft, e
+  | LocalAssum _ :: ctx -> aux (lft + 1) (subs_lift e) (subs_lift args) ctx
+  | LocalDef (_, c, _) :: ctx ->
+    let c = Vars.subst_instance_constr u c in
+    let c = mk_clos args c in
+    aux lft (subs_cons c e) (subs_cons c args) ctx
+  in
+  aux 0 e args (List.rev ctx)
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
   try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -672,13 +695,23 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         if Float64.equal f1 f2 then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
-    | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) ->
+    | FCaseInvert (ci1,u1,pms1,p1,_,_,br1,e1), FCaseInvert (ci2,u2,pms2,p2,_,_,br2,e2) ->
       (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible);
       let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in
-      let ccnv = ccnv CONV l2r infos el1 el2 in
-      let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in
-      Array.fold_right2 (fun b1 b2 cuniv -> ccnv (mk_clos e1 b1) (mk_clos e2 b2) cuniv)
-        br1 br2 cuniv
+      let fold c1 c2 cuniv = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
+      (** FIXME: cache the presence of let-bindings in the case_info *)
+      let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+      let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+      let cuniv =
+        let ind = (mind,snd ci1.ci_ind) in
+        let nargs = inductive_cumulativity_arguments ind in
+        convert_inductives CONV ind nargs u1 u2 cuniv
+      in
+      let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+      let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+      let cuniv = List.fold_right2 fold pms1 pms2 cuniv in
+      let cuniv = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 p1 p2 cuniv in
+      convert_branches ci1.ci_ind mind mip l2r infos e1 e2 el1 el2 u1 u2 pms1 pms2 br1 br2 cuniv
 
     | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
       let len = Parray.length_int t1 in
@@ -714,11 +747,27 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 let cu2 = f fx1 fx2 cu1 in
                 cmp_rec a1 a2 cu2
-            | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) ->
+            | (Zlcase(ci1,l1,u1,pms1,p1,br1,e1),Zlcase(ci2,l2,u2,pms2,p2,br2,e2)) ->
                 if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then
                   raise NotConvertible;
-                let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in
-                convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2
+                let cu = cu1 in
+                (** FIXME: cache the presence of let-bindings in the case_info *)
+                let mind = Environ.lookup_mind (fst ci1.ci_ind) (info_env infos.cnv_inf) in
+                let mip = mind.Declarations.mind_packets.(snd ci1.ci_ind) in
+                let cu =
+                  if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+                    convert_instances ~flex:false u1 u2 cu
+                  else
+                    match mind.Declarations.mind_variance with
+                    | None -> convert_instances ~flex:false u1 u2 cu
+                    | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
+                in
+                let pms1 = Array.map_to_list (fun c -> mk_clos e1 c) pms1 in
+                let pms2 = Array.map_to_list (fun c -> mk_clos e2 c) pms2 in
+                let fold_params c1 c2 accu = f (l1, c1) (l2, c2) accu in
+                let cu = List.fold_right2 fold_params pms1 pms2 cu in
+                let cu = convert_return_clause ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu in
+                convert_branches ci1.ci_ind mind mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 br1 br2 cu
             | (Zlprimitive(op1,_,rargs1,kargs1),Zlprimitive(op2,_,rargs2,kargs2)) ->
               if not (CPrimitives.equal op1 op2) then raise NotConvertible else
                 let cu2 = List.fold_right2 f rargs1 rargs2 cu1 in
@@ -743,21 +792,55 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv =
-  (** Skip comparison of the pattern types. We know that the two terms are
-      living in a common type, thus this check is useless. *)
-  let fold n c1 c2 cuniv = match skip_pattern infos n c1 c2 with
-  | (infos, c1, c2) ->
-    let lft1 = el_liftn n lft1 in
-    let lft2 = el_liftn n lft2 in
+and convert_under_context l2r infos e1 e2 lft1 lft2 ctx (nas1, c1) (nas2, c2) cu =
+  let n = Array.length nas1 in
+  let () = assert (Int.equal n (Array.length nas2)) in
+  let n, e1, e2 = match ctx with
+  | None -> (* nolet *)
     let e1 = subs_liftn n e1 in
     let e2 = subs_liftn n e2 in
-    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
-  | exception IrregularPatternShape ->
-    (** Might happen due to a shape invariant that is not enforced *)
-    ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv
+    (n, e1, e2)
+  | Some (ctx, u1, u2, args1, args2) ->
+    let n1, e1 = esubst_of_rel_context_instance ctx u1 args1 e1 in
+    let n2, e2 = esubst_of_rel_context_instance ctx u2 args2 e2 in
+    let () = assert (Int.equal n1 n2) in
+    n1, e1, e2
+  in
+  let lft1 = el_liftn n lft1 in
+  let lft2 = el_liftn n lft2 in
+  let infos = push_relevances infos nas1 in
+  ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cu
+
+and convert_return_clause ind mib mip l2r infos e1 e2 l1 l2 u1 u2 pms1 pms2 p1 p2 cu =
+  let ctx =
+    if Int.equal mip.mind_nrealargs mip.mind_nrealdecls then None
+    else
+      let ctx, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
+      let pms1 = inductive_subst ind mib u1 pms1 in
+      let pms2 = inductive_subst ind mib u1 pms2 in
+      let open Context.Rel.Declaration in
+      (* Add the inductive binder *)
+      let dummy = mkProp in
+      let ctx = LocalAssum (Context.anonR, dummy) :: ctx in
+      Some (ctx, u1, u2, pms1, pms2)
+  in
+  convert_under_context l2r infos e1 e2 l1 l2 ctx p1 p2 cu
+
+and convert_branches ind mib mip l2r infos e1 e2 lft1 lft2 u1 u2 pms1 pms2 br1 br2 cuniv =
+  let fold i (ctx, _) cuniv =
+    let ctx =
+      if Int.equal mip.mind_consnrealdecls.(i) mip.mind_consnrealargs.(i) then None
+      else
+        let ctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
+        let pms1 = inductive_subst ind mib u1 pms1 in
+        let pms2 = inductive_subst ind mib u2 pms2 in
+        Some (ctx, u1, u2, pms1, pms2)
+    in
+    let c1 = br1.(i) in
+    let c2 = br2.(i) in
+    convert_under_context l2r infos e1 e2 lft1 lft2 ctx c1 c2 cuniv
   in
-  Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv
+  Array.fold_right_i fold mip.mind_nf_lc cuniv
 
 and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
 | [], [] -> cuniv