From 6e0eed7075700d4c33a0193f6ec92c4d4bbebee8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 19 Oct 2021 21:22:10 +0200 Subject: [PATCH] Fix an issue with eliminator generation for nested where clauses --- examples/_CoqProject | 1 + examples/cartesian.v | 51 ++++++++++++++++++++++++++++++++++++++++++++ src/g_equations.mlg | 22 ++++++++++++++++--- src/principles.ml | 44 ++++++++++++++++++++++---------------- src/principles.mli | 2 +- src/splitting.ml | 28 ++++++++++++++++++++++-- test-suite/fin.v | 2 +- 7 files changed, 125 insertions(+), 25 deletions(-) create mode 100644 examples/cartesian.v diff --git a/examples/_CoqProject b/examples/_CoqProject index bbc262c7a..fbeded943 100644 --- a/examples/_CoqProject +++ b/examples/_CoqProject @@ -21,3 +21,4 @@ wfrec.v AlmostFull.v POPLMark1a.v bove_capretta.v +cartesian.v diff --git a/examples/cartesian.v b/examples/cartesian.v new file mode 100644 index 000000000..f2ee631c3 --- /dev/null +++ b/examples/cartesian.v @@ -0,0 +1,51 @@ +(* From an example by Olivier Danvy. *) +From Equations Require Import Equations. +From Coq Require Import List. + +Set Equations Transparent. +Import ListNotations. + +Section cart. + Context {A B : Type}. + (* No need to have the eliminator generalize over the A, B parameters *) + + Equations cartesian (v1s_given : list A) (v2s_given : list B) : list (A * B) := + cartesian v1s_given v2s_given := traverse_1 v1s_given + where traverse_1 (l : list A) : list (A * B) := + { | [] := [] + | (v1 :: v1s') := traverse_2 v2s_given + where traverse_2 (l : list B) : list (A * B) by struct l := + | [] := traverse_1 v1s' + | (v2 :: v2s') := (v1, v2) :: traverse_2 v2s' }. +End cart. + +Lemma cartesian_spec {A B} (l : list A) (l' : list B) p : + In p (cartesian l l') <-> In (fst p) l /\ In (snd p) l'. +Proof. + revert p. pattern l, l', (cartesian l l'). + (* The bulk of the proof is here: the two invariants needed on the + two traversals. *) + unshelve eapply (cartesian_elim _ + (fun _ l' l r => forall p, In p r <-> In (fst p) l /\ In (snd p) l') + (fun _ v2s_given v1 v1s' v2s' r => forall p, In p r <-> (v1 = fst p /\ In (snd p) v2s') \/ + (In (fst p) v1s' /\ In (snd p) v2s_given))); auto. + all:cbn; intros; rewrite ?H; intuition auto; cbn. + - noconf H1. intuition auto. + - noconf H1. noconf H0. intuition auto. +Qed. + +(* Extraction cartesian. *) +(* +(** val cartesian : 'a1 list -> 'a2 list -> ('a1, 'a2) prod list **) + +let rec cartesian v1s_given v2s_given = + match v1s_given with + | Nil -> Nil + | Cons (y, l) -> + let rec traverse_2 = function + | Nil -> cartesian l v2s_given + | Cons (y0, l1) -> Cons ((Pair (y, y0)), (traverse_2 l1)) + in traverse_2 v2s_given +*) +Eval compute in cartesian [1; 2] [3; 4]. + diff --git a/src/g_equations.mlg b/src/g_equations.mlg index e9b1b94b6..eb64dfd41 100644 --- a/src/g_equations.mlg +++ b/src/g_equations.mlg @@ -376,13 +376,29 @@ GRAMMAR EXTEND Gram in aux l } ] ] ; + + letconstr: + [ [ (*"let"; id=lident; bl = binders; ty = OPT [ ":"; c = Constr.lconstr -> { c } ] ; ":="; + c1 = term LEVEL "200"; "in"; c2 = letconstr -> + { let ty,c1 = match ty, c1 with + | None, { CAst.v = Constrexpr.CCast(c, Glob_term.CastConv t) } -> Some t, c (* Tolerance, see G_vernac.def_body *) + | _, _ -> ty, c1 in + let (c, (w, wn)) = c2 in + let eqn : pre_equation = SignPats + (CAst.make ~loc (Constrexpr.CRef (Libnames.qualid_of_ident ~loc:(fst id) (snd id), None))), + Some (Program (ConstrExpr c1, ([], []))) in + let w' : pre_equation where_clause = ((id, None, None, bl, ty, None), [eqn]) in + (c, (w' :: w, wn)) } *) + c = Constr.lconstr; w = local_wheres -> { (ConstrExpr c, w) } + ] ] + ; rhs: [ [ ":=!"; id = identloc -> { Some (Empty id) } - | [":=" -> { () } |"=>" -> { () } ]; c = Constr.lconstr; w = local_wheres -> - { Some (Program (ConstrExpr c, w)) } + | [":=" -> { () } |"=>" -> { () } ]; c = letconstr -> + { let (ce, w) = c in Some (Program (ce, w)) } - | ["with" -> { () } ]; refs = refine; [":=" -> { () } |"=>" -> { () } ]; + | ["with" -> { () } ]; refs = refine; [":=" -> { () } |"=>" -> { () } ]; e = sub_equations -> { Some (Refine (refs, e)) } | -> { None } ] ] diff --git a/src/principles.ml b/src/principles.ml index 29b6248a9..3c971313c 100644 --- a/src/principles.ml +++ b/src/principles.ml @@ -618,14 +618,18 @@ let map_proto evd recarg f ty = | None -> f type rec_subst = (Names.Id.t * (int option * EConstr.constr)) list +let _prsubst env evd s = Pp.(prlist_with_sep spc (fun (id, (recarg, f)) -> + str (Id.to_string id) ++ str" -> " ++ Printer.pr_econstr_env env evd f) s) -let cut_problem evd s ctx = +let cut_problem env evd s ctx = (* From Γ, x := t, D |- id_subst (G, x, D) : G, x : _, D to oΓ, D[t] |- id_subst (G, D) | G[ ps, prec, ps' : Δ, rec, Δ', and s : prec -> Γ |- t : rec build Γ |- ps, ps' : Δ, Δ'[prec/rec] *) + (* Feedback.msg_debug Pp.(str"cut_problem on " ++ pr_context env evd ctx); + Feedback.msg_debug Pp.(str"with substitution " ++ prsubst env evd s); *) let rec fn s (ctxl, pats, ctxr as ctxm) = match s with | [] -> ctxm @@ -633,6 +637,9 @@ let cut_problem evd s ctx = try let rel, _, ty = Termops.lookup_rel_id id ctxr in let fK = map_proto evd recarg term (lift rel ty) in + (* Feedback.msg_debug Pp.(str"subst_in_ctx " ++ int rel ++ str" by " ++ + Printer.pr_econstr_env (push_rel_context ctxr env) evd fK ++ str " in " ++ + pr_context env evd ctxr); *) let ctxr' = subst_in_ctx rel fK ctxr in let left, right = CList.chop (pred rel) pats in let right' = List.tl right in @@ -645,13 +652,13 @@ let subst_rec env evd cutprob s (ctx, p, _ as lhs) = let subst = List.fold_left (fun (ctx, pats, ctx' as lhs') (id, (recarg, b)) -> try let rel, _, ty = Termops.lookup_rel_id id ctx in - (* Feedback.msg_debug Pp.(str"lhs': " ++ pr_context_map env evd lhs'); *) - let fK = map_proto evd recarg (mapping_constr evd lhs b) (lift rel ty) in + (* Feedback.msg_debug Pp.(str"lhs': " ++ pr_context_map env evd lhs'); *) + let fK = map_proto evd recarg (mapping_constr evd lhs' (mapping_constr evd lhs b)) (lift rel ty) in (* Feedback.msg_debug Pp.(str"fk: " ++ Printer.pr_econstr_env (push_rel_context ctx env) evd fK); *) let substf = single_subst env evd rel (PInac fK) ctx in (* ctx[n := f] |- _ : ctx *) let substctx = compose_subst env ~sigma:evd substf lhs' in - (* Feedback.msg_debug Pp.(str"substituted context: " ++ pr_context_map env evd substctx); *) + (* Feedback.msg_debug Pp.(str"substituted context: " ++ pr_context_map env evd substctx); *) substctx with Not_found (* lookup *) -> lhs') (id_subst ctx) s in @@ -743,13 +750,10 @@ let push_decls_map env evd (ctx : context_map) cut (g : rel_context) = let map, _ = List.fold_right (fun decl acc -> push_mapping_context env evd decl acc) g (ctx, cut) in check_ctx_map env evd map -let _prsubst env evd s = Pp.(prlist_with_sep spc (fun (id, (recarg, f)) -> - str (Id.to_string id) ++ str" -> " ++ Printer.pr_econstr_env env !evd f) s) - let subst_rec_programs env evd ps = let where_map = ref PathMap.empty in let evd = ref evd in - let cut_problem s ctx' = cut_problem !evd s ctx' in + let cut_problem s ctx' = cut_problem env !evd s ctx' in let subst_rec cutprob s lhs = subst_rec env !evd cutprob s lhs in let rec subst_programs path s ctxlen progs oterms = let fixsubst = @@ -769,8 +773,9 @@ let subst_rec_programs env evd ps = let lifts = List.map (fun (id, (recarg, b)) -> (id, (recarg, lift (List.length fixsubst) b))) s in let s' = fixsubst @ lifts in - (* Feedback.msg_debug Pp.(str"In subst_programs, pr_substs" ++ prsubst env evd s'); *) + (* Feedback.msg_debug Pp.(str"In subst_programs, s' = " ++ prsubst env !evd s'); *) let one_program p oterm = + (* Feedback.msg_debug Pp.(str"In subst_program, substituting in " ++ Id.print p.program_info.program_id); *) let rec_prob, rec_arity = match p.program_rec with | Some { rec_prob; rec_arity } -> rec_prob, rec_arity @@ -778,10 +783,10 @@ let subst_rec_programs env evd ps = in let prog_info = p.program_info in let cutprob_sign = cut_problem s prog_info.program_sign in - (* Feedback.msg_debug Pp.(str"In subst_programs: " ++ pr_context env !evd prog_info.program_sign); - * Feedback.msg_debug Pp.(str"In subst_programs: cutprob_sign " ++ pr_context_map env !evd cutprob_sign); *) + (* Feedback.msg_debug Pp.(str"In subst_programs: " ++ pr_context env !evd prog_info.program_sign); *) + (* Feedback.msg_debug Pp.(str"In subst_programs: cutprob_sign " ++ pr_context_map env !evd cutprob_sign); *) let cutprob_subst, _ = subst_rec cutprob_sign s (id_subst prog_info.program_sign) in - (* Feedback.msg_debug Pp.(str"In subst_programs: subst_rec failed " ++ pr_context env !evd prog_info.program_sign); *) + (* Feedback.msg_debug Pp.(str"In subst_programs: cutprob_subst " ++ pr_context_map env !evd cutprob_subst); *) let program_info' = { prog_info with program_rec = None; @@ -791,6 +796,7 @@ let subst_rec_programs env evd ps = let program' = { p with program_info = program_info' } in let path' = p.program_info.program_id :: path in (* Feedback.msg_debug Pp.(str"In subst_programs, cut_problem s'" ++ pr_context env !evd (pi1 rec_prob)); *) + (* Feedback.msg_debug Pp.(str"In subst_programs, s'" ++ prsubst env !evd s'); *) let rec_cutprob = cut_problem s' (pi1 rec_prob) in let splitting' = aux rec_cutprob s' program' oterm path' p.program_splitting @@ -815,20 +821,22 @@ let subst_rec_programs env evd ps = where_type} as w) (subst_wheres, wheres) = (* subst_wheres lives in lhs', i.e. has prototypes substituted already *) let wcontext = where_context subst_wheres in - let cutprob' = cut_problem s (pi3 subst) in - (* Feedback.msg_debug Pp.(str"where_context in subst rec : " ++ pr_context env !evd wcontext); - * Feedback.msg_debug Pp.(str"lifting subst : " ++ pr_context_map env !evd subst); + let wp = where_program in + (* Feedback.msg_debug Pp.(str"In aux compute, cut_problem for " ++ Id.print wp.program_info.program_id + ++ prsubst env !evd lhss); *) + let cutprob' = cut_problem lhss (pi3 subst) in + (* Feedback.msg_debug Pp.(str"lifting subst : " ++ pr_context_map env !evd subst); * Feedback.msg_debug Pp.(str"cutprob : " ++ pr_context_map env !evd cutprob'); *) let wsubst0 = push_decls_map env !evd subst cutprob' wcontext in (* Feedback.msg_debug Pp.(str"new substitution in subst rec : " ++ pr_context_map env !evd wsubst0); *) let ctxlen = List.length wcontext + List.length ctx in - let wp = where_program in let where_type = mapping_constr !evd wsubst0 where_type in (* The substituted prototypes must be lifted w.r.t. the new variables bound in this where and preceding ones. *) + (* Feedback.msg_debug Pp.(str"lifting substitution by " ++ int (List.length (pi1 wp.program_prob) - List.length ctx)); *) let s = List.map (fun (id, (recarg, b)) -> - (id, (recarg, lift ((* List.length subst_wheres + *) - List.length (pi1 wp.program_prob) - List.length ctx) b))) lhss in + (id, (recarg, lift (List.length wp.program_info.program_sign - List.length ctx) b))) lhss in + (* let _ = Feedback.msg_debug Pp.(str"new substitution " ++ prsubst env !evd s) in *) let wp' = match subst_programs path s ctxlen [wp] [where_term w] with | [wp'] -> wp' diff --git a/src/principles.mli b/src/principles.mli index b5a90ddb7..c3b8c4a3e 100644 --- a/src/principles.mli +++ b/src/principles.mli @@ -85,7 +85,7 @@ val unfold_constr : Evd.evar_map -> constr -> Proofview.V82.tac type rec_subst = (Names.Id.t * (int option * EConstr.constr)) list -val cut_problem : +val cut_problem : Environ.env -> Evd.evar_map -> rec_subst -> Equations_common.rel_declaration list -> Equations_common.rel_declaration list * Context_map.pat list * diff --git a/src/splitting.ml b/src/splitting.ml index 38df8c65d..78502f1e7 100644 --- a/src/splitting.ml +++ b/src/splitting.ml @@ -642,6 +642,11 @@ let term_of_tree env0 isevar sort tree = let term = EConstr.it_mkLambda_or_LetIn term ctx in let typ = it_mkProd_or_subst env evm ty ctx in let term = Evarutil.nf_evar !evd term in + if !Equations_common.debug then + Feedback.msg_debug (str"type checking case" ++ + Printer.pr_econstr_env env !evd term ++ spc () ++ + str"of type" ++ spc () ++ + Printer.pr_econstr_env env !evd typ); evd := Typing.check env !evd term typ; !evd, term, typ in @@ -697,18 +702,37 @@ let make_program env evd p prob s rec_info = [| beta_appvect !evd fn (extended_rel_vect 0 (pi1 lhs)) |] in Single (p, prob, rec_info, s, it_mkLambda_or_LetIn term (pi1 lhs)) | StructRec sr -> + if !Equations_common.debug then + Feedback.msg_debug (str"term_of_tree for" ++ pr_splitting env !evd s); let term, ty = term_of_tree env evd sort s in let args = extended_rel_vect 0 r.rec_lets in + let args_lets = rel_vect 0 (List.length r.rec_lets) in + if !Equations_common.debug then + Feedback.msg_debug (str"returned:" ++ Printer.pr_econstr_env env !evd term); let term = beta_appvect !evd term args in + if !Equations_common.debug then + Feedback.msg_debug (str"after beta:" ++ Printer.pr_econstr_env (push_rel_context r.rec_lets env) !evd term); let before, after = CList.chop r.rec_args r.rec_sign in let fixdecls, after = CList.chop sr.struct_rec_protos after in - let subst = List.append (List.map (fun _ -> mkProp) fixdecls) (List.rev (Array.to_list args)) in + let subst = List.append (List.map (fun _ -> mkProp) fixdecls) (List.rev (Array.to_list args_lets)) in let program_sign = subst_rel_context 0 subst before in - let program_arity = substnl subst r.rec_args r.rec_arity in + if !Equations_common.debug then + Feedback.msg_debug (str"rec_sign:" ++ pr_context env !evd r.rec_sign); + if !Equations_common.debug then + Feedback.msg_debug (str"program arity:" ++ Printer.pr_econstr_env env !evd r.rec_arity); + if !Equations_common.debug then + Feedback.msg_debug (str"rec_lets:" ++ pr_context env !evd r.rec_lets); + if !Equations_common.debug then + Feedback.msg_debug (str"rec_args:" ++ int r.rec_args); + let program_arity = substnl subst r.rec_args r.rec_arity in let p' = { p with program_sign; program_arity } in + if !Equations_common.debug then + Feedback.msg_debug (str"program_sign:" ++ pr_context (push_rel_context after env) !evd program_sign); + if !Equations_common.debug then + Feedback.msg_debug (str"program arity:" ++ Printer.pr_econstr_env env !evd program_arity); let p' = match p.program_rec with | Some (Structural ann) -> diff --git a/test-suite/fin.v b/test-suite/fin.v index 00ca70a81..ad96465e8 100644 --- a/test-suite/fin.v +++ b/test-suite/fin.v @@ -80,7 +80,7 @@ Set Program Mode. Equations? fin_to_nat_bound {n : nat} (i : fin n) : {m : nat | m < n} := fin_to_nat_bound fz := 0; -fin_to_nat_bound (fs j) := let (m, p) := fin_to_nat_bound j in (S m). +fin_to_nat_bound (fs j) with fin_to_nat_bound j := { | (exist _ m p) := (S m) }. Proof. - apply Le.le_n_S; apply Le.le_0_n. - apply Lt.lt_n_S; assumption.