UIP in SProp

9 files changed, 48 insertions, 30 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 42c9359ff0..32eb63a818 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -69,7 +69,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, r, p) = of_kind (Case (ci, c, r, p))
+let mkCase (ci, c, iv, r, p) = of_kind (Case (ci, 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))
@@ -194,7 +194,7 @@ let destCoFix sigma c = match kind sigma c with
 | _ -> raise DestKO
 
 let destCase sigma c = match kind sigma c with
-| Case (ci, t, c, p) -> (ci, t, c, p)
+| Case (ci, t, iv, c, p) -> (ci, t, iv, c, p)
 | _ -> raise DestKO
 
 let destProj sigma c = match kind sigma c with
@@ -356,7 +356,7 @@ 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,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
+  | Case (_,p,iv,c,bl) -> 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;
@@ -380,7 +380,7 @@ let compare_gen k eq_inst eq_sort eq_constr nargs c1 c2 =
 
 let eq_constr sigma c1 c2 =
   let kind c = kind sigma c in
-  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
   let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
   let rec eq_constr nargs c1 c2 =
     compare_gen kind eq_inst eq_sorts eq_constr nargs c1 c2
@@ -390,13 +390,13 @@ let eq_constr sigma c1 c2 =
 let eq_constr_nounivs sigma c1 c2 =
   let kind c = kind sigma c in
   let rec eq_constr nargs c1 c2 =
-    compare_gen kind (fun _ _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
+    compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr nargs c1 c2
   in
   eq_constr 0 c1 c2
 
 let compare_constr sigma cmp c1 c2 =
   let kind c = kind sigma c in
-  let eq_inst _ _ i1 i2 = EInstance.equal sigma i1 i2 in
+  let eq_inst _ i1 i2 = EInstance.equal sigma i1 i2 in
   let eq_sorts s1 s2 = ESorts.equal sigma s1 s2 in
   let cmp nargs c1 c2 = cmp c1 c2 in
   compare_gen kind eq_inst eq_sorts cmp 0 c1 c2
@@ -442,22 +442,22 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
       Array.fold_left2 (fun cstrs u1 u2 -> UnivProblem.(Set.add (UWeak (u1,u2)) cstrs))
         cstrs (Univ.Instance.to_array u1) (Univ.Instance.to_array u2)
 
-let eq_universes env sigma cstrs cv_pb ref nargs l l' =
+let eq_universes env sigma cstrs cv_pb refargs l l' =
   if EInstance.is_empty l then (assert (EInstance.is_empty l'); true)
   else
     let l = EInstance.kind sigma l
     and l' = EInstance.kind sigma l' in
     let open GlobRef in
     let open UnivProblem in
-    match ref with
-    | VarRef _ -> assert false (* variables don't have instances *)
-    | ConstRef _ ->
+    match refargs with
+    | None | Some (ConstRef _, _) ->
       cstrs := enforce_eq_instances_univs true l l' !cstrs; true
-    | IndRef ind ->
+    | Some (VarRef _, _) -> assert false (* variables don't have instances *)
+    | Some (IndRef ind, nargs) ->
       let mind = Environ.lookup_mind (fst ind) env in
       cstrs := cmp_inductives cv_pb (mind,snd ind) nargs l l' !cstrs;
       true
-    | ConstructRef ((mi,ind),ctor) ->
+    | Some (ConstructRef ((mi,ind),ctor), nargs) ->
       let mind = Environ.lookup_mind mi env in
       cstrs := cmp_constructors (mind,ind,ctor) nargs l l' !cstrs;
       true
@@ -469,8 +469,8 @@ let test_constr_universes env sigma leq m n =
   else
     let cstrs = ref Set.empty in
     let cv_pb = if leq then Reduction.CUMUL else Reduction.CONV in
-    let eq_universes ref nargs l l' = eq_universes env sigma cstrs Reduction.CONV ref nargs l l'
-    and leq_universes ref nargs l l' = eq_universes env sigma cstrs cv_pb ref nargs l l' in
+    let eq_universes refargs l l' = eq_universes env sigma cstrs Reduction.CONV refargs l l'
+    and leq_universes refargs l l' = eq_universes env sigma cstrs cv_pb refargs l l' in
     let eq_sorts s1 s2 =
       let s1 = ESorts.kind sigma s1 in
       let s2 = ESorts.kind sigma s2 in
@@ -777,5 +777,7 @@ let to_named_context =
     = fun Refl x -> x
   in
   gen unsafe_eq
+let to_case_invert = unsafe_to_case_invert
+
 let eq = unsafe_eq
 end
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index aea441b90b..2bf8f69af7 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -128,7 +128,7 @@ val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
 val mkConstructU : constructor * EInstance.t -> t
 val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * t * t array -> t
+val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
@@ -198,7 +198,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * t * t array
+val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
 val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -341,6 +341,8 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
 
 val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 
+val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
@@ -365,6 +367,8 @@ sig
   val to_instance : EInstance.t -> Univ.Instance.t
   (** Physical identity. Does not care for normalization. *)
 
+  val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)
 end
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index eea7e38f87..3458743c0e 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -143,7 +143,7 @@ let head_evar sigma c =
   let c = EConstr.Unsafe.to_constr c in
   let rec hrec c = match kind c with
     | Evar (evk,_)   -> evk
-    | Case (_,_,c,_) -> hrec c
+    | Case (_,_,_,c,_) -> hrec c
     | App (c,_)      -> hrec c
     | Cast (c,_,_)   -> hrec c
     | Proj (p, c)    -> hrec c
diff --git a/engine/evd.ml b/engine/evd.ml
index f0ee8ae68f..c570f75c6b 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1398,6 +1398,9 @@ module MiniEConstr = struct
   let unsafe_to_rel_decl d = d
   let to_rel_decl sigma d = Context.Rel.Declaration.map_constr (to_constr sigma) d
 
+  let unsafe_to_case_invert x = x
+  let of_case_invert x = x
+
 end
 
 (** The following functions return the set of evars immediately
diff --git a/engine/evd.mli b/engine/evd.mli
index d9b7bd76e7..679173ca72 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -732,6 +732,8 @@ module MiniEConstr : sig
     (Constr.t, Constr.types) Context.Named.Declaration.pt
   val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt ->
     (Constr.t, Constr.types) Context.Rel.Declaration.pt
+  val of_case_invert : (constr,Univ.Instance.t) case_invert -> (econstr,EInstance.t) case_invert
+  val unsafe_to_case_invert : (econstr,EInstance.t) case_invert -> (constr,Univ.Instance.t) case_invert
   val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt ->
     (t, t) Context.Rel.Declaration.pt
   val to_rel_decl : evar_map -> (t, t) Context.Rel.Declaration.pt ->
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c4472050f8..1cf5be10ae 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -118,7 +118,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *)
         Some (Nametab.basename_of_global (global_of_constr c))
     | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) ->
         Some (match lna.(i).binder_name with Name id -> id | _ -> assert false)
-    | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) | Int _ | Float _ -> None
+    | Sort _ | Rel _ | Meta _|Evar _|Case _ | Int _ | Float _ -> None
   in
   hdrec c
 
@@ -163,7 +163,7 @@ let hdchar env sigma c =
         let id = match lna.(i).binder_name with Name id -> id | _ -> assert false in
         lowercase_first_char id
     | Evar _ (* We could do better... *)
-    | Meta _ | Case (_, _, _, _) -> "y"
+    | Meta _ | Case _ -> "y"
     | Int _ -> "i"
     | Float _ -> "f"
   in
diff --git a/engine/termops.ml b/engine/termops.ml
index c51e753d46..f6d0807823 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -639,13 +639,14 @@ let map_constr_with_binders_left_to_right sigma g f l c =
     let al' = List.map_left (f l) al in
       if List.for_all2 (==) al' al then c
       else mkEvar (e, al')
-  | Case (ci,p,b,bl) ->
+  | Case (ci,p,iv,b,bl) ->
       (* In v8 concrete syntax, predicate is after the term to match! *)
       let b' = f l b in
+      let iv' = map_invert (f l) iv in
       let p' = f l p in
       let bl' = Array.map_left (f l) bl in
-        if b' == b && p' == p && bl' == bl then c
-        else mkCase (ci, p', b', bl')
+      if b' == b && p' == p && iv' == iv && bl' == bl then c
+      else mkCase (ci, p', iv', b', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let l' = fold_rec_types g fx l in
       let (tl', bl') = map_left2 (f l) tl (f l') bl in
@@ -709,18 +710,20 @@ let map_constr_with_full_binders_gen userview sigma g f l cstr =
   | Evar (e,al) ->
       let al' = List.map (f l) al in
       if List.for_all2 (==) al al' then cstr else mkEvar (e, al')
-  | Case (ci,p,c,bl) when userview ->
+  | Case (ci,p,iv,c,bl) when userview ->
       let p' = map_return_predicate_with_full_binders sigma g f l ci p in
+      let iv' = map_invert (f l) iv in
       let c' = f l c in
       let bl' = map_branches_with_full_binders sigma g f l ci bl in
-      if p==p' && c==c' && bl'==bl then cstr else
-        mkCase (ci, p', c', bl')
-  | Case (ci,p,c,bl) ->
+      if p==p' && iv'==iv && c==c' && bl'==bl then cstr else
+        mkCase (ci, p', iv', c', bl')
+  | Case (ci,p,iv,c,bl) ->
       let p' = f l p in
+      let iv' = map_invert (f l) iv in
       let c' = f l c in
       let bl' = Array.map (f l) bl in
-      if p==p' && c==c' && Array.for_all2 (==) bl bl' then cstr else
-        mkCase (ci, p', c', bl')
+      if p==p' && iv'==iv && c==c' && Array.for_all2 (==) bl bl' then cstr else
+        mkCase (ci, p', iv', c', bl')
   | Fix (ln,(lna,tl,bl as fx)) ->
       let tl' = Array.map (f l) tl in
       let l' = fold_rec_types g fx l in
diff --git a/engine/univProblem.ml b/engine/univProblem.ml
index 08ff9efa5b..8d6689933c 100644
--- a/engine/univProblem.ml
+++ b/engine/univProblem.ml
@@ -150,7 +150,7 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu =
      [kind1,kind2], because [kind1] and [kind2] may be different,
      typically evaluating [m] and [n] in different evar maps. *)
   let cstrs = ref accu in
-  let eq_universes _ _ = UGraph.check_eq_instances univs in
+  let eq_universes _ = UGraph.check_eq_instances univs in
   let eq_sorts s1 s2 =
     if Sorts.equal s1 s2 then true
     else
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index 92211d5f3d..f06aeaf54e 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -146,7 +146,11 @@ let nf_evars_and_universes_opt_subst f subst =
         if pu' == pu then c else mkConstructU pu'
     | Sort (Type u) ->
       let u' = Univ.subst_univs_universe subst u in
-        if u' == u then c else mkSort (sort_of_univ u')
+      if u' == u then c else mkSort (sort_of_univ u')
+    | Case (ci,p,CaseInvert {univs;args},t,br) ->
+      let univs' = Instance.subst_fn lsubst univs in
+      if univs' == univs then Constr.map aux c
+      else Constr.map aux (mkCase (ci,p,CaseInvert {univs=univs';args},t,br))
     | _ -> Constr.map aux c
   in aux