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.
---
 engine/eConstr.ml | 94 +++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 78 insertions(+), 16 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index c29de27efb..ec255aad03 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -35,6 +35,10 @@ include (Evd.MiniEConstr : module type of Evd.MiniEConstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
+type case_invert = (t, EInstance.t) pcase_invert
+type case = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -69,7 +73,7 @@ let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
 let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
-let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, c, iv, r, p))
+let mkCase (ci, u, pms, c, iv, r, p) = of_kind (Case (ci, u, pms, c, iv, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
@@ -195,7 +199,7 @@ let destCoFix sigma c = match kind sigma c with
 | _ -> raise DestKO
 
 let destCase sigma c = match kind sigma c with
-| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
+| Case (ci, u, pms, t, iv, c, p) -> (ci, u, pms, t, iv, c, p)
 | _ -> raise DestKO
 
 let destProj sigma c = match kind sigma c with
@@ -320,19 +324,28 @@ let existential_type = Evd.existential_type
 
 let lift n c = of_constr (Vars.lift n (unsafe_to_constr c))
 
-let map_under_context f n c =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_under_context f n (unsafe_to_constr c))
-let map_branches f ci br =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr_array (Constr.map_branches f ci (unsafe_to_constr_array br))
-let map_return_predicate f ci p =
-  let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_return_predicate f ci (unsafe_to_constr p))
+let of_branches : Constr.case_branch array -> case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let unsafe_to_branches : case_branch array -> Constr.case_branch array =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let of_return : Constr.case_return -> case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
 
-let map_user_view sigma f c =
+let unsafe_to_return : case_return -> Constr.case_return =
+  match Evd.MiniEConstr.unsafe_eq with
+  | Refl -> fun x -> x
+
+let map_branches f br =
+  let f c = unsafe_to_constr (f (of_constr c)) in
+  of_branches (Constr.map_branches f (unsafe_to_branches br))
+let map_return_predicate f p =
   let f c = unsafe_to_constr (f (of_constr c)) in
-  of_constr (Constr.map_user_view f (unsafe_to_constr (whd_evar sigma c)))
+  of_return (Constr.map_return_predicate f (unsafe_to_return p))
 
 let map sigma f c =
   let f c = unsafe_to_constr (f (of_constr c)) in
@@ -346,7 +359,49 @@ let iter sigma f c =
   let f c = f (of_constr c) in
   Constr.iter f (unsafe_to_constr (whd_evar sigma c))
 
-let iter_with_full_binders sigma g f n c =
+let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let p = unsafe_to_return p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_branches bl in
+  let (ci, p, iv, c, bl) = Inductive.expand_case env (ci, u, pms, p, iv, c, bl) in
+  let p = of_constr p in
+  let c = of_constr c in
+  let iv = of_case_invert iv in
+  let bl = of_constr_array bl in
+  (ci, p, iv, c, bl)
+
+let expand_branch env _sigma u pms (ind, i) (nas, _br) =
+  let open Declarations in
+  let u = EInstance.unsafe_to_instance u in
+  let pms = unsafe_to_constr_array pms in
+  let (mib, mip) = Inductive.lookup_mind_specif env ind in
+  let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let paramsubst = Vars.subst_of_rel_context_instance paramdecl (Array.to_list pms) in
+  let subst = paramsubst @ Inductive.ind_subst (fst ind) mib u in
+  let (ctx, _) = mip.mind_nf_lc.(i - 1) in
+  let (ctx, _) = List.chop mip.mind_consnrealdecls.(i - 1) ctx in
+  let ans = Inductive.instantiate_context u subst nas ctx in
+  let ans : rel_context = match Evd.MiniEConstr.unsafe_eq with Refl -> ans in
+  ans
+
+let contract_case env _sigma (ci, p, iv, c, bl) =
+  let p = unsafe_to_constr p in
+  let iv = unsafe_to_case_invert iv in
+  let c = unsafe_to_constr c in
+  let bl = unsafe_to_constr_array bl in
+  let (ci, u, pms, p, iv, c, bl) = Inductive.contract_case env (ci, p, iv, c, bl) in
+  let u = EInstance.make u in
+  let pms = of_constr_array pms in
+  let p = of_return p in
+  let iv = of_case_invert iv in
+  let c = of_constr c in
+  let bl = of_branches bl in
+  (ci, u, pms, p, iv, c, bl)
+
+let iter_with_full_binders env sigma g f n c =
   let open Context.Rel.Declaration in
   match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
@@ -357,7 +412,10 @@ let iter_with_full_binders sigma g f n c =
   | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
-  | Case (_,p,iv,c,bl) -> f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+  | Case (ci,u,pms,p,iv,c,bl) ->
+    (* FIXME: skip the type annotations *)
+    let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in
+    f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
@@ -566,9 +624,13 @@ let universes_of_constr sigma c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
-    | Case (_,_,CaseInvert {univs;args=_},_,_) ->
+    | Case (_,u,_,_,CaseInvert {univs;args=_},_,_) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
       fold sigma aux s c
+    | Case (_, u, _, _, NoInvert, _, _) ->
+      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
+      fold sigma aux s c
     | _ -> fold sigma aux s c
   in aux LSet.empty c
 
-- 
cgit v1.2.3


From 0d7365e6ddcbd14933fcedae777649d31fb311cc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 15 Mar 2019 17:33:58 +0100
Subject: EConstr iterators respect the binding structure of cases.

Fixes #3166.
---
 engine/eConstr.ml | 18 +++++++++++++++---
 1 file changed, 15 insertions(+), 3 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ec255aad03..7748df1a9b 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -373,6 +373,18 @@ let expand_case env _sigma (ci, u, pms, p, iv, c, bl) =
   let bl = of_constr_array bl in
   (ci, p, iv, c, bl)
 
+let annotate_case env sigma (ci, u, pms, p, iv, c, bl as case) =
+  let (_, p, _, _, bl) = expand_case env sigma case in
+  let p =
+    (* Too bad we need to fetch this data in the environment, should be in the
+      case_info instead. *)
+    let (_, mip) = Inductive.lookup_mind_specif env ci.ci_ind in
+    decompose_lam_n_decls sigma (mip.Declarations.mind_nrealdecls + 1) p
+  in
+  let mk_br c n = decompose_lam_n_decls sigma n c in
+  let bl = Array.map2 mk_br bl ci.ci_cstr_ndecls in
+  (ci, u, pms, p, iv, c, bl)
+
 let expand_branch env _sigma u pms (ind, i) (nas, _br) =
   let open Declarations in
   let u = EInstance.unsafe_to_instance u in
@@ -413,9 +425,9 @@ let iter_with_full_binders env sigma g f n c =
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> List.iter (fun c -> f n c) l
   | Case (ci,u,pms,p,iv,c,bl) ->
-    (* FIXME: skip the type annotations *)
-    let (ci, p, iv, c, bl) = expand_case env sigma (ci, u, pms, p, iv, c, bl) in
-    f n p; iter_invert (f n) iv; f n c; Array.Fun1.iter f n bl
+    let (ci, _, pms, p, iv, c, bl) = annotate_case env sigma (ci, u, pms, p, iv, c, bl) in
+    let f_ctx (ctx, c) = f (List.fold_right g ctx n) c in
+    Array.Fun1.iter f n pms; f_ctx p; iter_invert (f n) iv; f n c; Array.iter f_ctx bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-- 
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

---
 engine/eConstr.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7748df1a9b..157995a173 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -37,7 +37,7 @@ type constr = t
 type existential = t pexistential
 type case_return = t pcase_return
 type case_branch = t pcase_branch
-type case_invert = (t, EInstance.t) pcase_invert
+type case_invert = t pcase_invert
 type case = (t, t, EInstance.t) pcase
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
@@ -636,11 +636,7 @@ let universes_of_constr sigma c =
     | Array (u,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
-    | Case (_,u,_,_,CaseInvert {univs;args=_},_,_) ->
-      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
-      let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in
-      fold sigma aux s c
-    | Case (_, u, _, _, NoInvert, _, _) ->
+    | Case (_,u,_,_,_,_,_) ->
       let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in
       fold sigma aux s c
     | _ -> fold sigma aux s c
-- 
cgit v1.2.3