Patterns: Accepting patterns in PFix and PCofix and not only constr.

4 files changed, 113 insertions, 47 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 19444988b..48ddd9496 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -14,7 +14,6 @@ open CErrors
 open Util
 open Names
 open Nameops
-open Constr
 open Termops
 open Libnames
 open Globnames
@@ -1223,8 +1222,36 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
 	| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
       in
       GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
-  | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
-  | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+  | PFix ((ln,i),(lna,tl,bl)) ->
+     let def_avoid, def_env, lfi =
+       Array.fold_left
+         (fun (avoid, env, l) na ->
+           let id = Namegen.next_name_away na avoid in
+           (Id.Set.add id avoid, Name id :: env, id::l))
+      (avoid, env, []) lna in
+     let n = Array.length tl in
+     let v = Array.map3
+               (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
+    bl tl ln in
+     GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+       Array.map (fun (bl,_,_) -> bl) v,
+       Array.map (fun (_,_,ty) -> ty) v,
+       Array.map (fun (_,bd,_) -> bd) v)
+  | PCoFix (ln,(lna,tl,bl)) ->
+     let def_avoid, def_env, lfi =
+       Array.fold_left
+         (fun (avoid, env, l) na ->
+           let id = Namegen.next_name_away na avoid in
+           (Id.Set.add id avoid, Name id :: env, id::l))
+         (avoid, env, []) lna in
+     let ntys = Array.length tl in
+     let v = Array.map2
+               (fun c t -> share_pattern_names glob_of_pat 0 [] def_avoid def_env sigma c (Patternops.lift_pattern ntys t))
+               bl tl in
+     GRec(GCoFix ln,Array.of_list (List.rev lfi),
+          Array.map (fun (bl,_,_) -> bl) v,
+          Array.map (fun (_,_,ty) -> ty) v,
+          Array.map (fun (_,bd,_) -> bd) v)
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
diff --git a/intf/pattern.ml b/intf/pattern.ml
index af2347674..76367b612 100644
--- a/intf/pattern.ml
+++ b/intf/pattern.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Globnames
-open Constr
 open Misctypes
 
 (** {5 Patterns} *)
@@ -37,8 +36,8 @@ type constr_pattern =
   | 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 *)
-  | PFix of fixpoint
-  | PCoFix of cofixpoint
+  | 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)
 
 (** Nota : in a [PCase], the array of branches might be shorter than
     expected, denoting the use of a final "_ => _" branch *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 888c76e3d..89d490a41 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -183,9 +183,36 @@ let push_binder na1 na2 t ctx =
      Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
   (na1, id2, t) :: ctx
 
-let to_fix (idx, (nas, cs, ts)) =
-  let inj = EConstr.of_constr in
-  (idx, (nas, Array.map inj cs, Array.map inj ts))
+(* This is an optimization of the main pattern-matching which shares
+   the longest common prefix of the body and type of a fixpoint. The
+   only practical effect at the time of writing is in binding variable
+   names: these variable names must be bound only once since the user
+   view at a fix displays only a (maximal) shared common prefix *)
+
+let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 =
+  match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with
+  | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') ->
+     let ctx = push_binder na1 na2 c2 ctx in
+     let ctx' = push_binder na1 na2' c2' ctx' in
+     let env = EConstr.push_rel (LocalAssum (na2,c2)) env in
+     let subst = sorec ctx env subst c1 c2 in
+     let subst = sorec ctx env subst c1' c2' in
+     let subst = add_binders na1 na2 binding_vars subst in
+     match_under_common_fix_binders sorec sigma binding_vars
+       ctx ctx' env env' subst t1' t2' b1' b2'
+  | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) ->
+     let ctx = push_binder na1 na2 u2 ctx in
+     let ctx' = push_binder na1 na2' u2' ctx' in
+     let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in
+     let subst = sorec ctx env subst c1 c2 in
+     let subst = sorec ctx env subst c1' c2' in
+     let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in
+     let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in
+     let subst = add_binders na1 na2 binding_vars subst in
+     match_under_common_fix_binders sorec sigma binding_vars
+       ctx ctx' env env' subst t1 t2 b1 b2
+  | _ ->
+     sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2
 
 let merge_binding sigma allow_bound_rels ctx n cT subst =
   let c = match ctx with
@@ -364,8 +391,20 @@ let matches_core env sigma allow_bound_rels
 	  let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
 	  List.fold_left chk_branch chk_head br1
 
-      |	PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
-      |	PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
+      |	PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
+           when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
+          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
+      |	PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2))
+           when i1 = i2 ->
+          let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+          let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+          let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+          Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
       | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
          Array.fold_left2 (sorec ctx env) subst args1 args2
       | (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index d69e41428..a0635c24a 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,16 +338,16 @@ 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'
+  | 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 mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped