diff options
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 49 | ||||
| -rw-r--r-- | test-suite/bugs/closed/7092.v | 70 |
3 files changed, 122 insertions, 1 deletions
@@ -6,6 +6,10 @@ Tools - Coq_makefile lets one override or extend the following variables from the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS. +Tactic language + +- Support for fix/cofix added in Ltac "match" and "lazymatch". + Changes from 8.7.2 to 8.8+beta1 =============================== diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index a0635c24a..e52112fda 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -349,9 +349,25 @@ let rec subst_pattern subst pat = 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 let warn_cast_in_pattern = @@ -451,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 -> 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. |