From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: 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.
---
 kernel/cooking.ml | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 3707a75157..930efa5d36 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,30 +75,30 @@ let share_univs cache r u l =
   let (u', args) = share cache r l in
     mkApp (instantiate_my_gr r (Instance.append u' u), args)
 
-let update_case cache ci iv modlist =
-  match share cache (IndRef ci.ci_ind) modlist with
-  | exception Not_found -> ci, iv
-  | u, l ->
-    let iv = match iv with
-      | NoInvert -> NoInvert
-      | CaseInvert {univs; args;} ->
-        let univs = Instance.append u univs in
-        let args = Array.append l args in
-        CaseInvert {univs; args;}
-    in
-    { ci with ci_npar = ci.ci_npar + Array.length l }, iv
-
 let is_empty_modlist (cm, mm) =
   Cmap.is_empty cm && Mindmap.is_empty mm
 
 let expmod_constr cache modlist c =
   let share_univs = share_univs cache in
-  let update_case = update_case cache in
   let rec substrec c =
     match kind c with
-      | Case (ci,p,iv,t,br) ->
-        let ci,iv = update_case ci iv modlist in
-        Constr.map substrec (mkCase (ci,p,iv,t,br))
+      | Case (ci, u, pms, p, iv, t, br) ->
+        begin match share cache (IndRef ci.ci_ind) modlist with
+        | (u', prefix) ->
+          let u = Instance.append u' u in
+          let pms = Array.append prefix pms in
+          let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
+          let iv = match iv with
+            | NoInvert -> NoInvert
+            | CaseInvert {univs; args;} ->
+              let univs = Instance.append u' univs in
+              let args = Array.append prefix args in
+              CaseInvert {univs; args;}
+          in
+          Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
+        | exception Not_found ->
+          Constr.map substrec c
+        end
 
       | Ind (ind,u) ->
           (try
-- 
cgit v1.2.3


From 868b948f8a7bd583d467c5d02dfb34d328d53d37 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 Dec 2020 13:20:54 +0100
Subject: Remove redundant univ and parameter info from CaseInvert

---
 kernel/cooking.ml | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 930efa5d36..f82b754c59 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -88,13 +88,6 @@ let expmod_constr cache modlist c =
           let u = Instance.append u' u in
           let pms = Array.append prefix pms in
           let ci = { ci with ci_npar = ci.ci_npar + Array.length prefix } in
-          let iv = match iv with
-            | NoInvert -> NoInvert
-            | CaseInvert {univs; args;} ->
-              let univs = Instance.append u' univs in
-              let args = Array.append prefix args in
-              CaseInvert {univs; args;}
-          in
           Constr.map substrec (mkCase (ci,u,pms,p,iv,t,br))
         | exception Not_found ->
           Constr.map substrec c
-- 
cgit v1.2.3