Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

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