Change the case representation of patterns.

5 files changed, 58 insertions, 61 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index c77feeafbb..c649e25d54 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -370,7 +370,7 @@ let matches_core env sigma allow_bound_rels
             raise PatternMatchingFailure
 
       | PCase (ci1, p1, a1, br1), Case (ci2, u2, pms2, p2, iv, a2, br2) ->
-          let (ci2, p2, _, a2, br2) = EConstr.expand_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
+          let (_, _, _, p2, _, _, br2) = EConstr.annotate_case env sigma (ci2, u2, pms2, p2, iv, a2, br2) in
           let n2 = Array.length br2 in
           let () = match ci1.cip_ind with
           | None -> ()
@@ -383,14 +383,29 @@ let matches_core env sigma allow_bound_rels
             if not ci1.cip_extensible && not (Int.equal (List.length br1) n2)
             then raise PatternMatchingFailure
           in
+          let sorec_under_ctx subst (n, c1) (decls, c2) =
+            let env = push_rel_context decls env in
+            let n = Array.rev_to_list n in
+            let fold na1 d (ctx, subst) =
+              let na2 = Context.Rel.Declaration.get_annot d in
+              let t = Context.Rel.Declaration.get_type d in
+              (push_binder na1 na2 t ctx, add_binders na1 na2 binding_vars subst)
+            in
+            let ctx, subst = List.fold_right2 fold n decls (ctx, subst) in
+            sorec ctx env subst c1 c2
+          in
           let chk_branch subst (j,n,c) =
             (* (ind,j+1) is normally known to be a correct constructor
                and br2 a correct match over the same inductive *)
             assert (j < n2);
-            sorec ctx env subst c br2.(j)
+            sorec_under_ctx subst (n, c) br2.(j)
+          in
+          let subst = sorec ctx env subst a1 a2 in
+          let subst = match p1 with
+          | None -> subst
+          | Some p1 -> sorec_under_ctx subst p1 p2
           in
-          let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
-          List.fold_left chk_branch chk_head br1
+          List.fold_left chk_branch subst br1
 
       |	PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
            when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index bb5125f5ed..722a0a2048 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -1160,18 +1160,3 @@ let rec subst_glob_constr env subst = DAst.map (function
           GArray(u,t',def',ty')
 
   )
-
-(* Utilities to transform kernel cases to simple pattern-matching problem *)
-
-let simple_cases_matrix_of_branches ind brs =
-  List.map (fun (i,n,b) ->
-      let nal,c = it_destRLambda_or_LetIn_names n b in
-      let mkPatVar na = DAst.make @@ PatVar na in
-      let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let ids = List.map_filter Nameops.Name.to_option nal in
-      CAst.make @@ (ids,[p],c))
-    brs
-
-let return_type_of_predicate ind nrealargs_tags pred =
-  let nal,p = it_destRLambda_or_LetIn_names (nrealargs_tags@[false]) pred in
-  (List.hd nal, Some (CAst.make (ind, List.tl nal))), Some p
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 254f772ff8..6d6f7fa97b 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -72,14 +72,6 @@ val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
 
-(** Utilities to transform kernel cases to simple pattern-matching problem *)
-
-val it_destRLambda_or_LetIn_names : bool list -> glob_constr -> Name.t list * glob_constr
-val simple_cases_matrix_of_branches :
-  inductive -> (int * bool list * glob_constr) list -> cases_clauses
-val return_type_of_predicate :
-  inductive -> bool list -> glob_constr -> predicate_pattern * glob_constr option
-
 val subst_genarg_hook :
   (substitution -> Genarg.glob_generic_argument -> Genarg.glob_generic_argument) Hook.t
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index f6d61f4892..553511f1bf 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -18,7 +18,6 @@ type patvar = Id.t
 type case_info_pattern =
     { cip_style : Constr.case_style;
       cip_ind : inductive option;
-      cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *)
       cip_extensible : bool (** does this match end with _ => _ ? *) }
 
 type constr_pattern =
@@ -35,8 +34,8 @@ type constr_pattern =
   | PSort of Sorts.family
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
-  | PCase of case_info_pattern * constr_pattern * constr_pattern *
-      (int * bool list * constr_pattern) list (** index of constructor, nb of args *)
+  | PCase of case_info_pattern * (Name.t array * constr_pattern) option * constr_pattern *
+      (int * Name.t array * constr_pattern) list (** index of constructor, nb of args *)
   | PFix of (int array * int) * (Name.t array * constr_pattern array * constr_pattern array)
   | PCoFix of int * (Name.t array * constr_pattern array * constr_pattern array)
   | PInt of Uint63.t
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 47097a0e32..0c4bbf71e2 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -24,7 +24,6 @@ open Environ
 let case_info_pattern_eq i1 i2 =
   i1.cip_style == i2.cip_style &&
   Option.equal Ind.CanOrd.equal i1.cip_ind i2.cip_ind &&
-  Option.equal (List.equal (==)) i1.cip_ind_tags i2.cip_ind_tags &&
   i1.cip_extensible == i2.cip_extensible
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
@@ -51,7 +50,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
   case_info_pattern_eq info1 info2 &&
-  constr_pattern_eq p1 p2 &&
+  Option.equal (fun (nas1, p1) (nas2, p2) -> Array.equal Name.equal nas1 nas2 && constr_pattern_eq p1 p2) p1 p2 &&
   constr_pattern_eq r1 r2 &&
   List.equal pattern_eq l1 l2
 | PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
@@ -74,7 +73,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 (** FIXME: fixpoint and cofixpoint should be relativized to pattern *)
 
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
-  Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
+  Int.equal i1 i2 && Array.equal Name.equal j1 j2 && constr_pattern_eq p1 p2
 
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal Name.equal n1 n2 &&
@@ -92,8 +91,8 @@ let rec occur_meta_pattern = function
   | PIf (c,c1,c2)  ->
       (occur_meta_pattern c) ||
       (occur_meta_pattern c1) || (occur_meta_pattern c2)
-  | PCase(_,p,c,br) ->
-      (occur_meta_pattern p) ||
+  | PCase(_, p,c,br) ->
+      Option.cata (fun (_, p) -> occur_meta_pattern p) false p ||
       (occur_meta_pattern c) ||
       (List.exists (fun (_,_,p) -> occur_meta_pattern p) br)
   | PArray (t,def,ty) ->
@@ -115,10 +114,10 @@ let rec occurn_pattern n = function
   | PIf (c,c1,c2)  ->
       (occurn_pattern n c) ||
       (occurn_pattern n c1) || (occurn_pattern n c2)
-  | PCase(_,p,c,br) ->
-      (occurn_pattern n p) ||
+  | PCase(_, p, c, br) ->
+      Option.cata (fun (nas, p) -> occurn_pattern (Array.length nas + n) p) false p ||
       (occurn_pattern n c) ||
-      (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+      (List.exists (fun (_, nas, p) -> occurn_pattern (Array.length nas + n) p) br)
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> List.exists (occurn_pattern n) args
   | PVar _ | PRef _ | PSort _ | PInt _ | PFloat _ -> false
@@ -202,18 +201,25 @@ let pattern_of_constr env sigma t =
       | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
       | _ ->
         PMeta None)
-    | Case (ci, u, pms, p, iv, a, br) ->
-        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p, iv, a, br) in
+    | Case (ci, u, pms, p0, iv, a, br0) ->
+        let (ci, p, iv, a, br) = Inductive.expand_case env (ci, u, pms, p0, iv, a, br0) in
+        let pattern_of_ctx c (nas, c0) =
+          let ctx, c = Term.decompose_lam_n_decls (Array.length nas) c in
+          let env = push_rel_context ctx env in
+          let c = pattern_of_constr env c in
+          (Array.map Context.binder_name nas, c)
+        in
+        let p = pattern_of_ctx p p0 in
         let cip =
           { cip_style = ci.ci_pp_info.style;
             cip_ind = Some ci.ci_ind;
-            cip_ind_tags = Some ci.ci_pp_info.ind_tags;
             cip_extensible = false }
         in
         let branch_of_constr i c =
-          (i, ci.ci_pp_info.cstr_tags.(i), pattern_of_constr env c)
+          let nas, c = pattern_of_ctx c br0.(i) in
+          (i, nas, c)
         in
-        PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
+        PCase (cip, Some p, pattern_of_constr env a,
                 Array.to_list (Array.mapi branch_of_constr br))
     | Fix (lni,(lna,tl,bl)) ->
        let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
@@ -242,7 +248,10 @@ let map_pattern_with_binders g f l = function
   | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) ->
-    PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
+    let fold nas l = Array.fold_left (fun l na -> g na l) l nas in
+    let map_branch (i, n, c) = (i, n, f (fold n l) c) in
+    let po = Option.map (fun (nas, po) -> nas, (f (fold nas l) po)) po in
+    PCase (ci,po,f l p, List.map map_branch pl)
   | PProj (p,pc) -> PProj (p, f l pc)
   | PFix (lni,(lna,tl,bl)) ->
      let l' = Array.fold_left (fun l na -> g na l) l lna in
@@ -352,7 +361,11 @@ let rec subst_pattern env sigma subst pat =
       let ind = cip.cip_ind in
       let ind' = Option.Smart.map (subst_ind subst) ind in
       let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
-      let typ' = subst_pattern env sigma subst typ in
+      let map ((nas, typ) as t) =
+        let typ' = subst_pattern env sigma subst typ in
+        if typ' == typ then t else (nas, typ')
+      in
+      let typ' = Option.Smart.map map typ in
       let c' = subst_pattern env sigma subst c in
       let subst_branch ((i,n,c) as br) =
         let c' = subst_pattern env sigma subst c in
@@ -382,8 +395,6 @@ let rec subst_pattern env sigma subst pat =
 let mkPLetIn na b t c = PLetIn(na,b,t,c)
 let mkPProd na t u = PProd(na,t,u)
 let mkPLambda na t b = PLambda(na,t,b)
-let mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped
 
 let mkPProd_or_LetIn (na,_,bo,t) c =
   match bo with
@@ -446,18 +457,14 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda na c = DAst.make ?loc @@
-        GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
-      let c = List.fold_right mkGLambda nal c in
       let cip =
         { cip_style = LetStyle;
           cip_ind = None;
-          cip_ind_tags = None;
           cip_extensible = false }
       in
-      let tags = List.map (fun _ -> false) nal (* Approximation which can be without let-ins... *) in
-      PCase (cip, PMeta None, pat_of_raw metas vars b,
-             [0,tags,pat_of_raw metas vars c])
+      let tags = Array.of_list nal (* Approximation which can be without let-ins... *) in
+      PCase (cip, None, pat_of_raw metas vars b,
+             [0,tags,pat_of_raw metas (List.rev_append (Array.to_list tags) vars) c])
   | GCases (sty,p,[c,(na,indnames)],brs) ->
       let get_ind p = match DAst.get p with
       | PatCstr((ind,_),_,_) -> Some ind
@@ -476,18 +483,17 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       let pred = match p,indnames with
         | Some p, Some {CAst.v=(_,nal)} ->
           let nvars = na :: List.rev nal @ vars in
-          rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
-        | None, _ -> PMeta None
+          Some (Array.rev_of_list (na :: List.rev nal), pat_of_raw metas nvars p)
+        | None, _ -> None
         | Some p, None ->
           match DAst.get p with
-          | GHole _ -> PMeta None
+          | GHole _ -> None
           | _ ->
             user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
         { cip_style = sty;
           cip_ind = ind;
-          cip_ind_tags = None;
           cip_extensible = ext }
       in
       (* Nota : when we have a non-trivial predicate,
@@ -556,10 +562,10 @@ and pats_of_glob_branches loc metas vars ind brs =
           err ?loc
             (str "No unique branch for " ++ int j ++ str"-th constructor.");
         let lna = List.map get_arg lv in
-        let vars' = List.rev lna @ vars in
-        let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in
+        let vars' = List.rev_append lna vars in
+        let tags = Array.of_list lna in
+        let pat = pat_of_raw metas vars' br in
         let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
-        let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
         ext, ((j-1, tags, pat) :: pats)
       | _ ->
         err ?loc:loc' (Pp.str "Non supported pattern.")