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, 12 insertions, 6 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6869f9c47e..0cad192332 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -672,9 +672,11 @@ let rec extract_term env sg mle mlt c args =
         (* we unify it with an fresh copy of the stored type of [Rel n]. *)
         let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
         in extract_app env sg mle mlt extract_rel args
-    | Case ({ci_ind=ip},_,iv,c0,br) ->
-      (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
-      extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
+    | Case (ci, u, pms, r, iv, c0, br) ->
+        (* If invert_case then this is a match that will get erased later, but right now we don't care. *)
+        let (ip, r, iv, c0, br) = EConstr.expand_case env sg (ci, u, pms, r, iv, c0, br) in
+        let ip = ci.ci_ind in
+        extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
         extract_app env sg mle mlt (extract_fix env sg mle i recd) args
     | CoFix (i,recd) ->
@@ -1078,9 +1080,13 @@ let fake_match_projection env p =
         let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg:arg lab in
         fold (arg+1) (j+1) (mkProj (Projection.make kn false, mkRel 1)::subst) rem
       else
-        let p = mkLambda (x, lift 1 indty, liftn 1 2 ty) in
-        let branch = lift 1 (it_mkLambda_or_LetIn (mkRel (List.length ctx - (j-1))) ctx) in
-        let body = mkCase (ci, p, NoInvert, mkRel 1, [|branch|]) in
+        let p = ([|x|], liftn 1 2 ty) in
+        let branch =
+          let nas = Array.of_list (List.rev_map Context.Rel.Declaration.get_annot ctx) in
+          (nas, mkRel (List.length ctx - (j - 1)))
+        in
+        let params = Context.Rel.to_extended_vect mkRel 1 paramslet in
+        let body = mkCase (ci, u, params, p, NoInvert, mkRel 1, [|branch|]) in
         it_mkLambda_or_LetIn (mkLambda (x,indty,body)) mib.mind_params_ctxt
     | LocalDef (_,c,t) :: rem ->
       let c = liftn 1 j c in