aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES4
-rw-r--r--clib/cArray.ml12
-rw-r--r--clib/cArray.mli2
-rw-r--r--interp/constrextern.ml33
-rw-r--r--intf/pattern.ml5
-rw-r--r--pretyping/constr_matching.ml49
-rw-r--r--pretyping/detyping.ml163
-rw-r--r--pretyping/detyping.mli7
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--pretyping/patternops.ml132
-rw-r--r--test-suite/bugs/closed/7092.v70
11 files changed, 355 insertions, 124 deletions
diff --git a/CHANGES b/CHANGES
index d982e0af7..37d9d3680 100644
--- a/CHANGES
+++ b/CHANGES
@@ -11,6 +11,10 @@ Vernacular Commands
- Removed deprecated commands Arguments Scope and Implicit Arguments
(not the option). Use the Arguments command instead.
+Tactic language
+
+- Support for fix/cofix added in Ltac "match" and "lazymatch".
+
Changes from 8.7.2 to 8.8+beta1
===============================
diff --git a/clib/cArray.ml b/clib/cArray.ml
index b6c033f6d..5eb20bc16 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -41,6 +41,8 @@ sig
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :
('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
+ val fold_left4 :
+ ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a
val fold_left2_i :
(int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
@@ -267,6 +269,16 @@ let fold_left3 f a v1 v2 v3 =
invalid_arg "Array.fold_left2";
fold a 0
+let fold_left4 f a v1 v2 v3 v4 =
+ let lv1 = Array.length v1 in
+ let rec fold a n =
+ if n >= lv1 then a
+ else fold (f a (uget v1 n) (uget v2 n) (uget v3 n) (uget v4 n)) (succ n)
+ in
+ if Array.length v2 <> lv1 || Array.length v3 <> lv1 || Array.length v4 <> lv1 then
+ invalid_arg "Array.fold_left4";
+ fold a 0
+
let fold_left_from n f a v =
let len = Array.length v in
let () = if n < 0 then invalid_arg "Array.fold_left_from" in
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 97038b0ac..f4f60f8aa 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -66,6 +66,8 @@ sig
('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left3 :
('a -> 'b -> 'c -> 'd -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'a
+ val fold_left4 :
+ ('a -> 'b -> 'c -> 'd -> 'e -> 'a) -> 'a -> 'b array -> 'c array -> 'd array -> 'e array -> 'a
val fold_left2_i :
(int -> 'a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a
val fold_left_from : int -> ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a
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/detyping.ml b/pretyping/detyping.ml
index 587892141..bb563220b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
let eqnl = detype_eqns constructs constagsl bl in
GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+let rec share_names detype n l avoid env sigma c t =
+ match EConstr.kind sigma c, EConstr.kind sigma t with
+ (* factorize even when not necessary to have better presentation *)
+ | Lambda (na,t,c), Prod (na',t',c') ->
+ let na = match (na,na') with
+ Name _, _ -> na
+ | _, Name _ -> na'
+ | _ -> na in
+ let t' = detype avoid env sigma t in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
+ share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+ (* May occur for fix built interactively *)
+ | LetIn (na,b,t',c), _ when n > 0 ->
+ let t'' = detype avoid env sigma t' in
+ let b' = detype avoid env sigma b in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
+ share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+ (* Only if built with the f/n notation or w/o let-expansion in types *)
+ | _, LetIn (_,b,_,t) when n > 0 ->
+ share_names detype n l avoid env sigma c (subst1 b t)
+ (* If it is an open proof: we cheat and eta-expand *)
+ | _, Prod (na',t',c') when n > 0 ->
+ let t'' = detype avoid env sigma t' in
+ let id = next_name_away na' avoid in
+ let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
+ let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+ share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+ (* If built with the f/n notation: we renounce to share names *)
+ | _ ->
+ if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+
+let rec share_pattern_names detype n l avoid env sigma c t =
+ let open Pattern in
+ if n = 0 then
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+ else match c, t with
+ | PLambda (na,t,c), PProd (na',t',c') ->
+ let na = match (na,na') with
+ Name _, _ -> na
+ | _, Name _ -> na'
+ | _ -> na in
+ let t' = detype avoid env sigma t in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set.add id avoid in
+ let env = Name id :: env in
+ share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+ | _ ->
+ if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+
+let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+ let def_avoid, def_env, lfi =
+ Array.fold_left2
+ (fun (avoid, env, l) na ty ->
+ let id = next_name_away na avoid in
+ (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+ (avoid, env, []) names tys in
+ let n = Array.length tys in
+ let v = Array.map3
+ (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t))
+ bodies tys vn in
+ GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+
+let detype_cofix detype avoid env sigma n (names,tys,bodies) =
+ let def_avoid, def_env, lfi =
+ Array.fold_left2
+ (fun (avoid, env, l) na ty ->
+ let id = next_name_away na avoid in
+ (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+ (avoid, env, []) names tys in
+ let ntys = Array.length tys in
+ let v = Array.map2
+ (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t))
+ bodies tys in
+ GRec(GCoFix n,Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+
let detype_universe sigma u =
let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
Univ.Universe.map fn u
@@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t =
(ci.ci_ind,ci.ci_pp_info.style,
ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
p c bl
- | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
- | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
-
-and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
- let def_avoid, def_env, lfi =
- Array.fold_left2
- (fun (avoid, env, l) na ty ->
- let id = next_name_away na avoid in
- (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
- (avoid, env, []) names tys in
- let n = Array.length tys in
- let v = Array.map3
- (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t))
- bodies tys vn in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
- Array.map (fun (bl,_,_) -> bl) v,
- Array.map (fun (_,_,ty) -> ty) v,
- Array.map (fun (_,bd,_) -> bd) v)
-
-and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
- let def_avoid, def_env, lfi =
- Array.fold_left2
- (fun (avoid, env, l) na ty ->
- let id = next_name_away na avoid in
- (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
- (avoid, env, []) names tys in
- let ntys = Array.length tys in
- let v = Array.map2
- (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t))
- bodies tys in
- GRec(GCoFix n,Array.of_list (List.rev lfi),
- Array.map (fun (bl,_,_) -> bl) v,
- Array.map (fun (_,_,ty) -> ty) v,
- Array.map (fun (_,bd,_) -> bd) v)
-
-and share_names d flags n l avoid env sigma c t =
- match EConstr.kind sigma c, EConstr.kind sigma t with
- (* factorize even when not necessary to have better presentation *)
- | Lambda (na,t,c), Prod (na',t',c') ->
- let na = match (na,na') with
- Name _, _ -> na
- | _, Name _ -> na'
- | _ -> na in
- let t' = detype d flags avoid env sigma t in
- let id = next_name_away na avoid in
- let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
- share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
- (* May occur for fix built interactively *)
- | LetIn (na,b,t',c), _ when n > 0 ->
- let t'' = detype d flags avoid env sigma t' in
- let b' = detype d flags avoid env sigma b in
- let id = next_name_away na avoid in
- let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
- share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
- (* Only if built with the f/n notation or w/o let-expansion in types *)
- | _, LetIn (_,b,_,t) when n > 0 ->
- share_names d flags n l avoid env sigma c (subst1 b t)
- (* If it is an open proof: we cheat and eta-expand *)
- | _, Prod (na',t',c') when n > 0 ->
- let t'' = detype d flags avoid env sigma t' in
- let id = next_name_away na' avoid in
- let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
- let appc = mkApp (lift 1 c,[|mkRel 1|]) in
- share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
- (* If built with the f/n notation: we renounce to share names *)
- | _ ->
- if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
- let c = detype d flags avoid env sigma c in
- let t = detype d flags avoid env sigma t in
- (List.rev l,c,t)
+ | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
+ | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
try
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 32b94e1b0..817b8ba6e 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort
val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) ->
evar_map -> rel_context -> 'a glob_decl_g list
+val share_pattern_names :
+ (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
+ (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list ->
+ Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
+ Pattern.constr_pattern ->
+ (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a
+
val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
(** look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 74f2cefab..e89bbf7c3 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
f m1 m2 && Name.equal pat1 pat2 &&
Option.equal f p1 p2 && f c1 c2 && f t1 t2
- | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
+ | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
Array.equal f c1 c2 && Array.equal f t1 t2
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index dcb93bfb6..e52112fda 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)
diff --git a/test-suite/bugs/closed/7092.v b/test-suite/bugs/closed/7092.v
new file mode 100644
index 000000000..d90de8b93
--- /dev/null
+++ b/test-suite/bugs/closed/7092.v
@@ -0,0 +1,70 @@
+(* Examples matching fix/cofix in Ltac pattern-matching *)
+
+Goal True.
+lazymatch (eval cbv delta [Nat.add] in Nat.add) with
+| (fix F (n : nat) (v : ?A) {struct n} : @?P n v
+ := match n with
+ | O => @?O_case v
+ | S n' => @?S_case n' v F
+ end)
+ =>
+ unify A nat;
+ unify P (fun _ _ : nat => nat);
+ unify O_case (fun v : nat => v);
+ unify S_case (fun (p : nat) (m : nat) (add : nat -> nat -> nat)
+ => S (add p m))
+ end.
+Abort.
+
+Fixpoint f l n := match n with 0 => 0 | S n => g n (cons n l) end
+with g n l := match n with 0 => 1 | S n => f (cons 0 l) n end.
+
+Goal True.
+
+lazymatch (eval cbv delta [f] in f) with
+| fix myf (l : ?L) (n : ?N) {struct n} : nat :=
+ match n as _ with
+ | 0 => ?Z
+ | S n0 => @?S myf myg n0 l
+ end
+ with myg (n' : ?N') (l' : ?L') {struct n'} : nat :=
+ match n' as _ with
+ | 0 => ?Z'
+ | S n0' => @?S' myf myg n0' l'
+ end
+ for myf =>
+ unify L (list nat);
+ unify L' (list nat);
+ unify N nat;
+ unify N' nat;
+ unify Z 0;
+ unify Z' 1;
+ unify S (fun (f : L -> N -> nat) (g : N -> L -> nat) n l => g n (cons n l));
+ unify S' (fun (f : L -> N -> nat) (g : N -> L -> nat) (n:N) l => f (cons 0 l) n)
+end.
+
+Abort.
+
+CoInductive S1 := C1 : nat -> S2 -> S1 with S2 := C2 : bool -> S1 -> S2.
+
+CoFixpoint f' n l := C1 n (g' (cons n l) n n)
+with g' l n p := C2 true (f' (S n) l).
+
+Goal True.
+
+lazymatch (eval cbv delta [f'] in f') with
+| cofix myf (n : ?N) (l : ?L) : ?T := @?X n g l
+ with g (l' : ?L') (n' : ?N') (p' : ?N'') : ?T' := @?X' n' myf l'
+ for myf =>
+ unify L (list nat);
+ unify L' (list nat);
+ unify N nat;
+ unify N' nat;
+ unify N'' nat;
+ unify T S1;
+ unify T' S2;
+ unify X (fun n g l => C1 n (g (cons n l) n n));
+ unify X' (fun n f (l : list nat) => C2 true (f (S n) l))
+end.
+
+Abort.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 08:17:33 +0000