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/vars.ml | 37 +++++++++++++++++++++++++++++--------
 1 file changed, 29 insertions(+), 8 deletions(-)

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index a446fa413c..0f71057787 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,12 +253,21 @@ let subst_univs_level_constr subst c =
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci,p,CaseInvert {univs;args},c,br) ->
-        if Univ.Instance.is_empty univs then Constr.map aux t
+      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+        if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
         else
+          let u' = f u in
           let univs' = f univs in
-          if univs' == univs then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br)))
+          if u' == u && univs' == univs then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+
+      | Case (ci, u, pms, p, NoInvert, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
+        else
+          let u' = f u in
+          if u' == u then Constr.map aux t
+          else
+            (changed := true; Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br)))
 
       | Array (u,elems,def,ty) ->
         let u' = f u in
@@ -305,10 +314,19 @@ let subst_instance_constr subst c =
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci,p,CaseInvert {univs;args},c,br) ->
+      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+        let u' = f u in
         let univs' = f univs in
-        if univs' == univs then Constr.map aux t
-        else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},c,br))
+        if u' == u && univs' == univs then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+
+      | Case (ci, u, pms, p, NoInvert, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
+        else
+          let u' = f u in
+          if u' == u then Constr.map aux t
+          else
+            Constr.map aux (mkCase (ci, u', pms, p, NoInvert, c, br))
 
       | Array (u,elems,def,ty) ->
         let u' = f u in
@@ -348,8 +366,11 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
-    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+    | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+      let s = LSet.fold LSet.add (Instance.levels u) s in
       let s = LSet.fold LSet.add (Instance.levels univs) s in
       Constr.fold aux s c
+    | Case (_, u, _, _, NoInvert, _, _) ->
+      Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
-- 
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/vars.ml | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index 0f71057787..b09577d4db 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -253,13 +253,12 @@ let subst_univs_level_constr subst c =
            if u' == u then t else
              (changed := true; mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
-        if Univ.Instance.is_empty u && Univ.Instance.is_empty univs then Constr.map aux t
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
+        if Univ.Instance.is_empty u then Constr.map aux t
         else
           let u' = f u in
-          let univs' = f univs in
-          if u' == u && univs' == univs then Constr.map aux t
-          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br)))
+          if u' == u then Constr.map aux t
+          else (changed:=true; Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br)))
 
       | Case (ci, u, pms, p, NoInvert, c, br) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -314,11 +313,10 @@ let subst_instance_constr subst c =
           if u' == u then t else
             (mkSort (Sorts.sort_of_univ u'))
 
-      | Case (ci, u, pms, p, CaseInvert {univs;args}, c, br) ->
+      | Case (ci, u, pms, p, CaseInvert {indices}, c, br) ->
         let u' = f u in
-        let univs' = f univs in
-        if u' == u && univs' == univs then Constr.map aux t
-        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {univs=univs';args},c,br))
+        if u' == u then Constr.map aux t
+        else Constr.map aux (mkCase (ci,u',pms,p,CaseInvert {indices},c,br))
 
       | Case (ci, u, pms, p, NoInvert, c, br) ->
         if Univ.Instance.is_empty u then Constr.map aux t
@@ -366,11 +364,8 @@ let universes_of_constr c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, CaseInvert {univs;args=_},_ ,_) ->
+    | Case (_, u, _, _, _,_ ,_) ->
       let s = LSet.fold LSet.add (Instance.levels u) s in
-      let s = LSet.fold LSet.add (Instance.levels univs) s in
       Constr.fold aux s c
-    | Case (_, u, _, _, NoInvert, _, _) ->
-      Constr.fold aux (LSet.fold LSet.add (Instance.levels u) s) c
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
-- 
cgit v1.2.3