Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)

1 files changed, 90 insertions, 42 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index dcb93bfb62..e52112fda0 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -15,7 +15,6 @@ open Globnames
 open Nameops
 open Term
 open Constr
-open Vars
 open Glob_term
 open Pp
 open Mod_subst
@@ -57,10 +56,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   constr_pattern_eq p1 p2 &&
   constr_pattern_eq r1 r2 &&
   List.equal pattern_eq l1 l2
-| PFix f1, PFix f2 ->
-  fixpoint_eq f1 f2
-| PCoFix f1, PCoFix f2 ->
-  cofixpoint_eq f1 f2
+| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
+  Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2
+| PCoFix (i1,f1), PCoFix (i2,f2) ->
+  Int.equal i1 i2 && rec_declaration_eq f1 f2
 | PProj (p1, t1), PProj (p2, t2) ->
    Projection.equal p1 p2 && constr_pattern_eq t1 t2
 | (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
@@ -71,19 +70,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 and pattern_eq (i1, j1, p1) (i2, j2, p2) =
   Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
 
-and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
-  Int.equal i1 i2 &&
-  Array.equal Int.equal arg1 arg2 &&
-  rec_declaration_eq r1 r2
-
-and cofixpoint_eq (i1, r1) (i2, r2) =
-  Int.equal i1 i2 &&
-  rec_declaration_eq r1 r2
-
 and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
   Array.equal Name.equal n1 n2 &&
-  Array.equal Constr.equal c1 c2 &&
-  Array.equal Constr.equal r1 r2
+  Array.equal constr_pattern_eq c1 c2 &&
+  Array.equal constr_pattern_eq r1 r2
 
 let rec occur_meta_pattern = function
   | PApp (f,args) ->
@@ -123,8 +113,10 @@ let rec occurn_pattern n = function
   | PMeta _ | PSoApp _ -> true
   | PEvar (_,args) -> Array.exists (occurn_pattern n) args
   | PVar _ | PRef _ | PSort _ -> false
-  | PFix fix -> not (noccurn n (mkFix fix))
-  | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+  | PFix (_,(_,tl,bl)) ->
+     Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
+  | PCoFix (_,(_,tl,bl)) ->
+     Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
 
 let noccurn_pattern n c = not (occurn_pattern n c)
 
@@ -209,8 +201,16 @@ let pattern_of_constr env sigma t =
 	in
 	PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
 	       Array.to_list (Array.mapi branch_of_constr br))
-    | Fix f -> PFix f
-    | CoFix f -> PCoFix f in
+    | Fix (lni,(lna,tl,bl)) ->
+       let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+       let env' = Array.fold_left2 push env lna tl in
+       PFix (lni,(lna,Array.map (pattern_of_constr env) tl,
+                  Array.map (pattern_of_constr env') bl))
+    | CoFix (ln,(lna,tl,bl)) ->
+       let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+       let env' = Array.fold_left2 push env lna tl in
+       PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl,
+                  Array.map (pattern_of_constr env') bl)) in
   pattern_of_constr env t
 
 (* To process patterns, we need a translation without typing at all. *)
@@ -225,10 +225,14 @@ let map_pattern_with_binders g f l = function
   | 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)
   | 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
+     PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl))
+  | PCoFix (ln,(lna,tl,bl)) ->
+     let l' = Array.fold_left (fun l na -> g na l) l lna in
+     PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
   (* Non recursive *)
-  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _
-  (* Bound to terms *)
-  | PFix _ | PCoFix _ as x) -> x
+  | (PVar _ | PEvar _ | PRel _ | PRef _  | PSort _  | PMeta _ as x) -> x
 
 let error_instantiate_pattern id l =
   let is = match l with
@@ -262,15 +266,12 @@ let instantiate_pattern env sigma lvar c =
 	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
        with Not_found (* Map.find failed *) ->
 	 x)
-  | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
   | c ->
       map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
   aux [] c
 
 let rec liftn_pattern k n = function
   | PRel i as x -> if i >= n then PRel (i+k) else x
-  | PFix x -> PFix (destFix (liftn k n (mkFix x)))
-  | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
   | c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
 
 let lift_pattern k = liftn_pattern k 1
@@ -337,19 +338,35 @@ let rec subst_pattern subst pat =
       if cip' == cip && typ' == typ && c' == c && branches' == branches
       then pat
       else PCase(cip', typ', c', branches')
-  | PFix fixpoint ->
-      let cstr = mkFix fixpoint in
-      let fixpoint' = destFix (subst_mps subst cstr) in
-	if fixpoint' == fixpoint then pat else
-	  PFix fixpoint'
-  | PCoFix cofixpoint ->
-      let cstr = mkCoFix cofixpoint in
-      let cofixpoint' = destCoFix (subst_mps subst cstr) in
-	if cofixpoint' == cofixpoint then pat else
-	  PCoFix cofixpoint'
-
-let mkPLambda na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambda = List.fold_right mkPLambda
+  | PFix (lni,(lna,tl,bl)) ->
+      let tl' = Array.smartmap (subst_pattern subst) tl in
+      let bl' = Array.smartmap (subst_pattern subst) bl in
+      if bl' == bl && tl' == tl then pat
+      else PFix (lni,(lna,tl',bl'))
+  | PCoFix (ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap (subst_pattern subst) tl in
+      let bl' = Array.smartmap (subst_pattern subst) bl in
+      if bl' == bl && tl' == tl then pat
+      else PCoFix (ln,(lna,tl',bl'))
+
+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
+  | None -> mkPProd na t c
+  | Some b -> mkPLetIn na b (Some t) c
+
+let mkPLambda_or_LetIn (na,_,bo,t) c =
+  match bo with
+  | None -> mkPLambda na t c
+  | Some b -> mkPLetIn na b (Some t) c
+
+let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c)
+let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c)
 
 let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
 
@@ -428,7 +445,7 @@ 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_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
+          rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
         | None, _ -> PMeta None
 	| Some p, None ->
           match DAst.get p with
@@ -450,9 +467,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
   | GProj(p,c) ->
     PProj(p, pat_of_raw metas vars c)
 
-  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+  | GRec (GFix (ln,n), ids, decls, tl, cl) ->
+    if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
+      err ?loc (Pp.str "\"struct\" annotation is expected.")
+    else
+      let ln = Array.map (fst %> Option.get) ln in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+      let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+      let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+      let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+      let names = Array.map (fun id -> Name id) ids in
+      PFix ((ln,n), (names, tl, cl))
+
+  | GRec (GCoFix n, ids, decls, tl, cl) ->
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+      let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+      let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+      let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+      let names = Array.map (fun id -> Name id) ids in
+      PCoFix (n, (names, tl, cl))
+
+  | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
       err ?loc (Pp.str "Non supported pattern."))
 
+and pat_of_glob_in_context metas vars decls c =
+  let rec aux acc vars = function
+    | (na,bk,b,t) :: decls ->
+       let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in
+       aux (decl::acc) (na::vars) decls
+    | [] ->
+       acc, pat_of_raw metas vars c
+  in aux [] vars decls
+
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg p = match DAst.get p with
     | PatVar na ->
@@ -477,7 +525,7 @@ and pats_of_glob_branches loc metas vars ind brs =
             (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_mkPLambda lna (pat_of_raw metas vars' br) in
+        let pat = rev_it_mkPLambdaUntyped lna (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)