From 72094961d9bd7f0f618d30b2b508d8924336d7b4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Jul 2016 10:47:17 +0200 Subject: Program: Move ProofIrrelevance to Subset.v --- theories/Program/Equality.v | 5 ++--- theories/Program/Subset.v | 1 + 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index a349eb9085..d6f9bb9df0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -8,7 +8,6 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Export ProofIrrelevance. Require Export JMeq. Require Import Coq.Program.Tactics. @@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p := | [ H : X = Y |- _ ] => match p with | H => fail 2 - | _ => rewrite (proof_irrelevance (X = Y) p H) + | _ => rewrite (UIP _ X Y p H) end | _ => fail " No hypothesis with same type " end @@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. apply proof_irrelevance. Qed. +Proof. apply UIP. Qed. Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c8f37318d1..2a3ec926b2 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,6 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. +Require Export ProofIrrelevance. Local Open Scope program_scope. -- cgit v1.2.3 From 4c0c4b46993aeb31786d60cb278cfb317dea454e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Jul 2016 11:49:06 +0200 Subject: Add test for pi_eq_proofs. --- test-suite/success/programequality.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 test-suite/success/programequality.v diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v new file mode 100644 index 0000000000..414c572f81 --- /dev/null +++ b/test-suite/success/programequality.v @@ -0,0 +1,13 @@ +Require Import Program. + +Axiom t : nat -> Set. + +Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type) + (a : t x), + P (eq_rect _ _ a _ e) e'. +Proof. + intros. + pi_eq_proofs. clear e. + destruct e'. simpl. + change (P a eq_refl). +Abort. \ No newline at end of file -- cgit v1.2.3 From 6c65822cd241ea2f5c552f8b685490aed86eecb1 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 16 Aug 2016 17:25:43 +0200 Subject: Output a break before a list only if there was an empty line (bug #4606). Moreover, this commit makes sure that an empty line after a list is always translated into a break. ("StartLevel 1" was excluded, for some reason.) It also avoids some code duplication. In particular, "stop_item ()" is defined as "reach_item_level 0", so there is no reason to handle "StartLevel 1" specially. --- tools/coqdoc/cpretty.mll | 30 +++++++----------------------- 1 file changed, 7 insertions(+), 23 deletions(-) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 9191b2acac..6cf1eaae17 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -681,7 +681,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -742,24 +742,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -769,6 +752,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -777,10 +764,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> -- cgit v1.2.3 From 8e79ac5a766e42dfbfc629087455c9bd7639402c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Aug 2016 09:33:03 +0200 Subject: infoH: output via msg_* to make the XML protocol happy --- proofs/refiner.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 14493458cf..ef4cfb158d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -218,7 +218,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc) "" lh)) "" newhyps in - pp (str (emacs_str "") + msg_notice (str (emacs_str "") ++ (hov 0 (str s)) ++ (str (emacs_str "")) ++ fnl()); tclIDTAC goal;; -- cgit v1.2.3 From 02bcddbba985b65ac167f63b48bf2bd5bceffa1f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Aug 2016 15:08:38 +0200 Subject: Fix #4978: priorities of Equivalence instances --- theories/Classes/Equivalence.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index c458894795..80b0b7e4c6 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv. +Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1. -Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv. +Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1. -Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv. +Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1. Next Obligation. Proof. intros A R sa x y z Hxy Hyz. @@ -123,7 +123,7 @@ Section Respecting. End Respecting. -(** The default equivalence on function spaces, with higher-priority than [eq]. *) +(** The default equivalence on function spaces, with higher priority than [eq]. *) Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) : Reflexive (pointwise_relation A eqB) | 9. -- cgit v1.2.3 From d1052e2d9e14684db1f86a9b419d388a8e70728c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Aug 2016 17:57:45 +0200 Subject: Documenting fix of #3070 (subst and chain of dependencies). --- CHANGES | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGES b/CHANGES index a9942d3a17..8f873bd91c 100644 --- a/CHANGES +++ b/CHANGES @@ -13,6 +13,7 @@ Bugfixes - #4592, #4932: notations sharing recursive patterns or sharing binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. +- #3070: fixing "subst" in the presence of a chain of dependencies. Specification language -- cgit v1.2.3 From 5ef642ad47de7ff465ea2d5456c387fd35409539 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 31 Jul 2016 15:49:29 +0200 Subject: Fixing CHANGES. Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section. --- CHANGES | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index c74aa7234c..de9dc649cb 100644 --- a/CHANGES +++ b/CHANGES @@ -533,6 +533,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1071,9 +1074,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions -- cgit v1.2.3 From 86935e33e8f5d4fcc4b5603086d594431a002d0b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 17 Aug 2016 17:52:12 +0200 Subject: Fixing #5001 (metas not cleaned properly in clenv_refine_in). Fixing by copying what Matthieu did for Clenvtac.clenv_refine. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e151a06583..54977dbce7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1095,7 +1095,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac -- cgit v1.2.3 From 745df84bc3f32a646f6010a0b40a42023aae9cf9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Aug 2016 16:31:32 +0200 Subject: Fix setoid_rewrite to raise proper errors when the rewrite lemma doesn't typecheck or does not correspond to a relation. --- ltac/rewrite.ml | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 47c78ae5c2..7acad20d20 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -1440,17 +1440,8 @@ let rewrite_with l2r flags c occs : strategy = { strategy = fun ({ state = () } as input) -> let unify env evars t = let (sigma, cstrs) = evars in - let ans = - try Some (refresh_hypinfo env sigma c) - with e when Class_tactics.catchable e -> None - in - match ans with - | None -> None - | Some (sigma, rew) -> - let rew = unify_eqn rew l2r flags env (sigma, cstrs) None t in - match rew with - | None -> None - | Some rew -> Some rew + let (sigma, rew) = refresh_hypinfo env sigma c in + unify_eqn rew l2r flags env (sigma, cstrs) None t in let app = apply_rule unify occs in let strat = -- cgit v1.2.3 From 982e239e2befe925410a08459053c7dc69c948a7 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 17 Aug 2016 17:14:55 -0400 Subject: In docs, fix command to reset Ltac profiling --- doc/refman/RefMan-ltac.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5ba3c308a6..9fbff7181e 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1277,7 +1277,7 @@ Prints the profile Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name. \begin{quote} -{\tt Reset Profile}. +{\tt Reset Ltac Profile}. \end{quote} Resets the profile, that is, deletes all accumulated information -- cgit v1.2.3 From 4b14558683a9fc6d0e0f1b5018bfbafc94bb8d3a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 18 Aug 2016 12:09:42 +0200 Subject: Adding a test for bug #4653. --- test-suite/bugs/closed/4653.v | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 test-suite/bugs/closed/4653.v diff --git a/test-suite/bugs/closed/4653.v b/test-suite/bugs/closed/4653.v new file mode 100644 index 0000000000..4514342c5e --- /dev/null +++ b/test-suite/bugs/closed/4653.v @@ -0,0 +1,3 @@ +Definition T := Type. +Module Type S. Parameter foo : let A := T in True. End S. +Module M <: S. Lemma foo (A := T) : True. Proof I. End M. -- cgit v1.2.3 From ce9058b597fc53310619d537aadacc091755ed39 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 18 Aug 2016 13:15:42 +0200 Subject: Fix bug #4939: LtacProf prints tactic notations weirdly. --- ltac/profile_ltac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index f332e1a0d5..bea02e3dcb 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -139,7 +139,7 @@ let string_of_call ck = let s = string_of_ppcmds (match ck with - | Tacexpr.LtacNotationCall s -> Names.KerName.print s + | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id | Tacexpr.LtacAtomCall te -> -- cgit v1.2.3 From 0d0e9738fa5ec96be85796e5cb8486de00018155 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 18 Aug 2016 16:27:59 +0200 Subject: Fix an occurrence of deprecated eqn syntax in stdlib. --- theories/Reals/Sqrt_reg.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 10527442e8..d43baee8cd 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -339,7 +339,7 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs. unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. rewrite Rabs_right. -- cgit v1.2.3 From 262ad3c3ce24463094110aa011471213ac0b61c7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 18 Aug 2016 18:47:55 +0200 Subject: Fix incorrect glob data for module symbols (bug #2336). The logic was backward: if the path of a symbol was a prefix of the current path, then the current path (without sections) was used. But what we want is that, if the current path (without sections) is a prefix of the path of a symbol, then the former should be used. This fixes about 1,600 broken links in the documentation of the standard library. --- interp/dumpglob.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 85212b7aba..d70d30d9ec 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir -- cgit v1.2.3 From c85e668255c1a2ef7881a7a106bffebd8f171f28 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 19 Aug 2016 07:05:18 +0200 Subject: Fix anomaly on user-inputted projection name (bug #5029). --- interp/constrintern.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c4688f9fb..30016dedcf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1078,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1094,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) -- cgit v1.2.3 From 283579ff70d324296e2b7ee2535b1187ca32e0cb Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 19 Aug 2016 07:38:25 +0200 Subject: Remove extraneous dot in error message (bug #4832). --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/equality.ml b/tactics/equality.ml index 819a995db1..06a9b317a2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -610,7 +610,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in -- cgit v1.2.3 From dd9ee0c788556640f47a797814ffddba76ae540f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Aug 2016 14:18:50 +0200 Subject: Moving Taccoerce to ltac/ folder. This was an overlook. There was no reason to let it in the tactics/ folder, as is was semantically part of the Ltac implementation. --- ltac/ltac.mllib | 1 + ltac/taccoerce.ml | 344 ++++++++++++++++++++++++++++++++++++++++++++++++++ ltac/taccoerce.mli | 96 ++++++++++++++ tactics/taccoerce.ml | 344 -------------------------------------------------- tactics/taccoerce.mli | 96 -------------- tactics/tactics.mllib | 1 - 6 files changed, 441 insertions(+), 441 deletions(-) create mode 100644 ltac/taccoerce.ml create mode 100644 ltac/taccoerce.mli delete mode 100644 tactics/taccoerce.ml delete mode 100644 tactics/taccoerce.mli diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 65ed114cff..fc51e48ae4 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Taccoerce Tacsubst Tacenv Tactic_debug diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml new file mode 100644 index 0000000000..0110510d35 --- /dev/null +++ b/ltac/taccoerce.ml @@ -0,0 +1,344 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t +| _ -> assert false + +let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> + let Val.Dyn (t, _) = v in + match Val.eq t (val_tag wit) with + | None -> false + | Some Refl -> true + +let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> + let Val.Dyn (t', x) = v in + match Val.eq t t' with + | None -> None + | Some Refl -> Some x + +let in_gen wit v = Val.Dyn (val_tag wit, v) +let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x + +module Value = +struct + +type t = Val.t + +let normalize v = v + +let of_constr c = in_gen (topwit wit_constr) c + +let to_constr v = + let v = normalize v in + if has_type v (topwit wit_constr) then + let c = out_gen (topwit wit_constr) v in + Some c + else if has_type v (topwit wit_constr_under_binders) then + let vars, c = out_gen (topwit wit_constr_under_binders) v in + match vars with [] -> Some c | _ -> None + else None + +let of_uconstr c = in_gen (topwit wit_uconstr) c + +let to_uconstr v = + let v = normalize v in + if has_type v (topwit wit_uconstr) then + Some (out_gen (topwit wit_uconstr) v) + else None + +let of_int i = in_gen (topwit wit_int) i + +let to_int v = + let v = normalize v in + if has_type v (topwit wit_int) then + Some (out_gen (topwit wit_int) v) + else None + +let to_list v = prj Val.typ_list v + +let to_option v = prj Val.typ_opt v + +let to_pair v = prj Val.typ_pair v + +end + +let is_variable env id = + Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env)) + +(* Transforms an id into a constr if possible, or fails with Not_found *) +let constr_of_id env id = + Term.mkVar (let _ = Environ.lookup_named id env in id) + +(* Gives the constr corresponding to a Constr_context tactic_arg *) +let coerce_to_constr_context v = + let v = Value.normalize v in + if has_type v (topwit wit_constr_context) then + out_gen (topwit wit_constr_context) v + else raise (CannotCoerceTo "a term context") + +(* Interprets an identifier which must be fresh *) +let coerce_var_to_ident fresh env v = + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "a fresh identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) v + else match Value.to_constr v with + | None -> fail () + | Some c -> + (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *) + if isVar c && not (fresh && is_variable env (destVar c)) then + destVar c + else fail () + + +(* Interprets, if possible, a constr to an identifier which may not + be fresh but suitable to be given to the fresh tactic. Works for + vars, constants, inductive, constructors and sorts. *) +let coerce_to_ident_not_fresh g env v = +let id_of_name = function + | Names.Anonymous -> Id.of_string "x" + | Names.Name x -> x in + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "an identifier") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + out_gen (topwit wit_var) v + else + match Value.to_constr v with + | None -> fail () + | Some c -> + match Constr.kind c with + | Var id -> id + | Meta m -> id_of_name (Evd.meta_name g m) + | Evar (kn,_) -> + begin match Evd.evar_ident kn g with + | None -> fail () + | Some id -> id + end + | Const (cst,_) -> Label.to_id (Constant.label cst) + | Construct (cstr,_) -> + let ref = Globnames.ConstructRef cstr in + let basename = Nametab.basename_of_global ref in + basename + | Ind (ind,_) -> + let ref = Globnames.IndRef ind in + let basename = Nametab.basename_of_global ref in + basename + | Sort s -> + begin + match s with + | Prop _ -> Label.to_id (Label.make "Prop") + | Type _ -> Label.to_id (Label.make "Type") + end + | _ -> fail() + + +let coerce_to_intro_pattern env v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + snd (out_gen (topwit wit_intro_pattern) v) + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + IntroNaming (IntroIdentifier id) + else match Value.to_constr v with + | Some c when isVar c -> + (* This happens e.g. in definitions like "Tac H = clear H; intro H" *) + (* but also in "destruct H as (H,H')" *) + IntroNaming (IntroIdentifier (destVar c)) + | _ -> raise (CannotCoerceTo "an introduction pattern") + +let coerce_to_intro_pattern_naming env v = + match coerce_to_intro_pattern env v with + | IntroNaming pat -> pat + | _ -> raise (CannotCoerceTo "a naming introduction pattern") + +let coerce_to_hint_base v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> Id.to_string id + | _ -> raise (CannotCoerceTo "a hint base name") + else raise (CannotCoerceTo "a hint base name") + +let coerce_to_int v = + let v = Value.normalize v in + if has_type v (topwit wit_int) then + out_gen (topwit wit_int) v + else raise (CannotCoerceTo "an integer") + +let coerce_to_constr env v = + let v = Value.normalize v in + let fail () = raise (CannotCoerceTo "a term") in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) -> + (try ([], constr_of_id env id) with Not_found -> fail ()) + | _ -> fail () + else if has_type v (topwit wit_constr) then + let c = out_gen (topwit wit_constr) v in + ([], c) + else if has_type v (topwit wit_constr_under_binders) then + out_gen (topwit wit_constr_under_binders) v + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + (try [], constr_of_id env id with Not_found -> fail ()) + else fail () + +let coerce_to_uconstr env v = + let v = Value.normalize v in + if has_type v (topwit wit_uconstr) then + out_gen (topwit wit_uconstr) v + else + raise (CannotCoerceTo "an untyped term") + +let coerce_to_closed_constr env v = + let ids,c = coerce_to_constr env v in + let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in + c + +let coerce_to_evaluable_ref env v = + let fail () = raise (CannotCoerceTo "an evaluable reference") in + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id + | _ -> fail () + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id + else fail () + else if has_type v (topwit wit_ref) then + let open Globnames in + let r = out_gen (topwit wit_ref) v in + match r with + | VarRef var -> EvalVarRef var + | ConstRef c -> EvalConstRef c + | IndRef _ | ConstructRef _ -> fail () + else + let ev = match Value.to_constr v with + | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) + | Some c when isVar c -> EvalVarRef (destVar c) + | _ -> fail () + in + if Tacred.is_evaluable env ev then ev else fail () + +let coerce_to_constr_list env v = + let v = Value.to_list v in + match v with + | Some l -> + let map v = coerce_to_closed_constr env v in + List.map map l + | None -> raise (CannotCoerceTo "a term list") + +let coerce_to_intro_pattern_list loc env v = + match Value.to_list v with + | None -> raise (CannotCoerceTo "an intro pattern list") + | Some l -> + let map v = (loc, coerce_to_intro_pattern env v) in + List.map map l + +let coerce_to_hyp env v = + let fail () = raise (CannotCoerceTo "a variable") in + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + match out_gen (topwit wit_intro_pattern) v with + | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id + | _ -> fail () + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + if is_variable env id then id else fail () + else match Value.to_constr v with + | Some c when isVar c -> destVar c + | _ -> fail () + +let coerce_to_hyp_list env v = + let v = Value.to_list v in + match v with + | Some l -> + let map n = coerce_to_hyp env n in + List.map map l + | None -> raise (CannotCoerceTo "a variable list") + +(* Interprets a qualified name *) +let coerce_to_reference env v = + let v = Value.normalize v in + match Value.to_constr v with + | Some c -> + begin + try Globnames.global_of_constr c + with Not_found -> raise (CannotCoerceTo "a reference") + end + | None -> raise (CannotCoerceTo "a reference") + +(* Quantified named or numbered hypothesis or hypothesis in context *) +(* (as in Inversion) *) +let coerce_to_quantified_hypothesis v = + let v = Value.normalize v in + if has_type v (topwit wit_intro_pattern) then + let v = out_gen (topwit wit_intro_pattern) v in + match v with + | _, IntroNaming (IntroIdentifier id) -> NamedHyp id + | _ -> raise (CannotCoerceTo "a quantified hypothesis") + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + NamedHyp id + else if has_type v (topwit wit_int) then + AnonHyp (out_gen (topwit wit_int) v) + else match Value.to_constr v with + | Some c when isVar c -> NamedHyp (destVar c) + | _ -> raise (CannotCoerceTo "a quantified hypothesis") + +(* Quantified named or numbered hypothesis or hypothesis in context *) +(* (as in Inversion) *) +let coerce_to_decl_or_quant_hyp env v = + let v = Value.normalize v in + if has_type v (topwit wit_int) then + AnonHyp (out_gen (topwit wit_int) v) + else + try coerce_to_quantified_hypothesis v + with CannotCoerceTo _ -> + raise (CannotCoerceTo "a declared or quantified hypothesis") + +let coerce_to_int_or_var_list v = + match Value.to_list v with + | None -> raise (CannotCoerceTo "an int list") + | Some l -> + let map n = ArgArg (coerce_to_int n) in + List.map map l diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli new file mode 100644 index 0000000000..0b67f8726e --- /dev/null +++ b/ltac/taccoerce.mli @@ -0,0 +1,96 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* t + (** Eliminated the leading dynamic type casts. *) + + val of_constr : constr -> t + val to_constr : t -> constr option + val of_uconstr : Glob_term.closed_glob_constr -> t + val to_uconstr : t -> Glob_term.closed_glob_constr option + val of_int : int -> t + val to_int : t -> int option + val to_list : t -> t list option + val to_option : t -> t option option + val to_pair : t -> (t * t) option +end + +(** {5 Coercion functions} *) + +val coerce_to_constr_context : Value.t -> constr + +val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t + +val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t + +val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr + +val coerce_to_intro_pattern_naming : + Environ.env -> Value.t -> intro_pattern_naming_expr + +val coerce_to_hint_base : Value.t -> string + +val coerce_to_int : Value.t -> int + +val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders + +val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr + +val coerce_to_closed_constr : Environ.env -> Value.t -> constr + +val coerce_to_evaluable_ref : + Environ.env -> Value.t -> evaluable_global_reference + +val coerce_to_constr_list : Environ.env -> Value.t -> constr list + +val coerce_to_intro_pattern_list : + Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns + +val coerce_to_hyp : Environ.env -> Value.t -> Id.t + +val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list + +val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference + +val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis + +val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis + +val coerce_to_int_or_var_list : Value.t -> int or_var list + +(** {5 Missing generic arguments} *) + +val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type + +val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml deleted file mode 100644 index 0110510d35..0000000000 --- a/tactics/taccoerce.ml +++ /dev/null @@ -1,344 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t -| _ -> assert false - -let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit -> - let Val.Dyn (t, _) = v in - match Val.eq t (val_tag wit) with - | None -> false - | Some Refl -> true - -let prj : type a. a Val.typ -> Val.t -> a option = fun t v -> - let Val.Dyn (t', x) = v in - match Val.eq t t' with - | None -> None - | Some Refl -> Some x - -let in_gen wit v = Val.Dyn (val_tag wit, v) -let out_gen wit v = match prj (val_tag wit) v with None -> assert false | Some x -> x - -module Value = -struct - -type t = Val.t - -let normalize v = v - -let of_constr c = in_gen (topwit wit_constr) c - -let to_constr v = - let v = normalize v in - if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in - Some c - else if has_type v (topwit wit_constr_under_binders) then - let vars, c = out_gen (topwit wit_constr_under_binders) v in - match vars with [] -> Some c | _ -> None - else None - -let of_uconstr c = in_gen (topwit wit_uconstr) c - -let to_uconstr v = - let v = normalize v in - if has_type v (topwit wit_uconstr) then - Some (out_gen (topwit wit_uconstr) v) - else None - -let of_int i = in_gen (topwit wit_int) i - -let to_int v = - let v = normalize v in - if has_type v (topwit wit_int) then - Some (out_gen (topwit wit_int) v) - else None - -let to_list v = prj Val.typ_list v - -let to_option v = prj Val.typ_opt v - -let to_pair v = prj Val.typ_pair v - -end - -let is_variable env id = - Id.List.mem id (Termops.ids_of_named_context (Environ.named_context env)) - -(* Transforms an id into a constr if possible, or fails with Not_found *) -let constr_of_id env id = - Term.mkVar (let _ = Environ.lookup_named id env in id) - -(* Gives the constr corresponding to a Constr_context tactic_arg *) -let coerce_to_constr_context v = - let v = Value.normalize v in - if has_type v (topwit wit_constr_context) then - out_gen (topwit wit_constr_context) v - else raise (CannotCoerceTo "a term context") - -(* Interprets an identifier which must be fresh *) -let coerce_var_to_ident fresh env v = - let v = Value.normalize v in - let fail () = raise (CannotCoerceTo "a fresh identifier") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> id - | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v - else match Value.to_constr v with - | None -> fail () - | Some c -> - (* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *) - if isVar c && not (fresh && is_variable env (destVar c)) then - destVar c - else fail () - - -(* Interprets, if possible, a constr to an identifier which may not - be fresh but suitable to be given to the fresh tactic. Works for - vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh g env v = -let id_of_name = function - | Names.Anonymous -> Id.of_string "x" - | Names.Name x -> x in - let v = Value.normalize v in - let fail () = raise (CannotCoerceTo "an identifier") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> id - | _ -> fail () - else if has_type v (topwit wit_var) then - out_gen (topwit wit_var) v - else - match Value.to_constr v with - | None -> fail () - | Some c -> - match Constr.kind c with - | Var id -> id - | Meta m -> id_of_name (Evd.meta_name g m) - | Evar (kn,_) -> - begin match Evd.evar_ident kn g with - | None -> fail () - | Some id -> id - end - | Const (cst,_) -> Label.to_id (Constant.label cst) - | Construct (cstr,_) -> - let ref = Globnames.ConstructRef cstr in - let basename = Nametab.basename_of_global ref in - basename - | Ind (ind,_) -> - let ref = Globnames.IndRef ind in - let basename = Nametab.basename_of_global ref in - basename - | Sort s -> - begin - match s with - | Prop _ -> Label.to_id (Label.make "Prop") - | Type _ -> Label.to_id (Label.make "Type") - end - | _ -> fail() - - -let coerce_to_intro_pattern env v = - let v = Value.normalize v in - if has_type v (topwit wit_intro_pattern) then - snd (out_gen (topwit wit_intro_pattern) v) - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - IntroNaming (IntroIdentifier id) - else match Value.to_constr v with - | Some c when isVar c -> - (* This happens e.g. in definitions like "Tac H = clear H; intro H" *) - (* but also in "destruct H as (H,H')" *) - IntroNaming (IntroIdentifier (destVar c)) - | _ -> raise (CannotCoerceTo "an introduction pattern") - -let coerce_to_intro_pattern_naming env v = - match coerce_to_intro_pattern env v with - | IntroNaming pat -> pat - | _ -> raise (CannotCoerceTo "a naming introduction pattern") - -let coerce_to_hint_base v = - let v = Value.normalize v in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> Id.to_string id - | _ -> raise (CannotCoerceTo "a hint base name") - else raise (CannotCoerceTo "a hint base name") - -let coerce_to_int v = - let v = Value.normalize v in - if has_type v (topwit wit_int) then - out_gen (topwit wit_int) v - else raise (CannotCoerceTo "an integer") - -let coerce_to_constr env v = - let v = Value.normalize v in - let fail () = raise (CannotCoerceTo "a term") in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) -> - (try ([], constr_of_id env id) with Not_found -> fail ()) - | _ -> fail () - else if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in - ([], c) - else if has_type v (topwit wit_constr_under_binders) then - out_gen (topwit wit_constr_under_binders) v - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - (try [], constr_of_id env id with Not_found -> fail ()) - else fail () - -let coerce_to_uconstr env v = - let v = Value.normalize v in - if has_type v (topwit wit_uconstr) then - out_gen (topwit wit_uconstr) v - else - raise (CannotCoerceTo "an untyped term") - -let coerce_to_closed_constr env v = - let ids,c = coerce_to_constr env v in - let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in - c - -let coerce_to_evaluable_ref env v = - let fail () = raise (CannotCoerceTo "an evaluable reference") in - let v = Value.normalize v in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id - | _ -> fail () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id - else fail () - else if has_type v (topwit wit_ref) then - let open Globnames in - let r = out_gen (topwit wit_ref) v in - match r with - | VarRef var -> EvalVarRef var - | ConstRef c -> EvalConstRef c - | IndRef _ | ConstructRef _ -> fail () - else - let ev = match Value.to_constr v with - | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) - | Some c when isVar c -> EvalVarRef (destVar c) - | _ -> fail () - in - if Tacred.is_evaluable env ev then ev else fail () - -let coerce_to_constr_list env v = - let v = Value.to_list v in - match v with - | Some l -> - let map v = coerce_to_closed_constr env v in - List.map map l - | None -> raise (CannotCoerceTo "a term list") - -let coerce_to_intro_pattern_list loc env v = - match Value.to_list v with - | None -> raise (CannotCoerceTo "an intro pattern list") - | Some l -> - let map v = (loc, coerce_to_intro_pattern env v) in - List.map map l - -let coerce_to_hyp env v = - let fail () = raise (CannotCoerceTo "a variable") in - let v = Value.normalize v in - if has_type v (topwit wit_intro_pattern) then - match out_gen (topwit wit_intro_pattern) v with - | _, IntroNaming (IntroIdentifier id) when is_variable env id -> id - | _ -> fail () - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - if is_variable env id then id else fail () - else match Value.to_constr v with - | Some c when isVar c -> destVar c - | _ -> fail () - -let coerce_to_hyp_list env v = - let v = Value.to_list v in - match v with - | Some l -> - let map n = coerce_to_hyp env n in - List.map map l - | None -> raise (CannotCoerceTo "a variable list") - -(* Interprets a qualified name *) -let coerce_to_reference env v = - let v = Value.normalize v in - match Value.to_constr v with - | Some c -> - begin - try Globnames.global_of_constr c - with Not_found -> raise (CannotCoerceTo "a reference") - end - | None -> raise (CannotCoerceTo "a reference") - -(* Quantified named or numbered hypothesis or hypothesis in context *) -(* (as in Inversion) *) -let coerce_to_quantified_hypothesis v = - let v = Value.normalize v in - if has_type v (topwit wit_intro_pattern) then - let v = out_gen (topwit wit_intro_pattern) v in - match v with - | _, IntroNaming (IntroIdentifier id) -> NamedHyp id - | _ -> raise (CannotCoerceTo "a quantified hypothesis") - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - NamedHyp id - else if has_type v (topwit wit_int) then - AnonHyp (out_gen (topwit wit_int) v) - else match Value.to_constr v with - | Some c when isVar c -> NamedHyp (destVar c) - | _ -> raise (CannotCoerceTo "a quantified hypothesis") - -(* Quantified named or numbered hypothesis or hypothesis in context *) -(* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env v = - let v = Value.normalize v in - if has_type v (topwit wit_int) then - AnonHyp (out_gen (topwit wit_int) v) - else - try coerce_to_quantified_hypothesis v - with CannotCoerceTo _ -> - raise (CannotCoerceTo "a declared or quantified hypothesis") - -let coerce_to_int_or_var_list v = - match Value.to_list v with - | None -> raise (CannotCoerceTo "an int list") - | Some l -> - let map n = ArgArg (coerce_to_int n) in - List.map map l diff --git a/tactics/taccoerce.mli b/tactics/taccoerce.mli deleted file mode 100644 index 0b67f8726e..0000000000 --- a/tactics/taccoerce.mli +++ /dev/null @@ -1,96 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* t - (** Eliminated the leading dynamic type casts. *) - - val of_constr : constr -> t - val to_constr : t -> constr option - val of_uconstr : Glob_term.closed_glob_constr -> t - val to_uconstr : t -> Glob_term.closed_glob_constr option - val of_int : int -> t - val to_int : t -> int option - val to_list : t -> t list option - val to_option : t -> t option option - val to_pair : t -> (t * t) option -end - -(** {5 Coercion functions} *) - -val coerce_to_constr_context : Value.t -> constr - -val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t - -val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t - -val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr - -val coerce_to_intro_pattern_naming : - Environ.env -> Value.t -> intro_pattern_naming_expr - -val coerce_to_hint_base : Value.t -> string - -val coerce_to_int : Value.t -> int - -val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders - -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr - -val coerce_to_closed_constr : Environ.env -> Value.t -> constr - -val coerce_to_evaluable_ref : - Environ.env -> Value.t -> evaluable_global_reference - -val coerce_to_constr_list : Environ.env -> Value.t -> constr list - -val coerce_to_intro_pattern_list : - Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns - -val coerce_to_hyp : Environ.env -> Value.t -> Id.t - -val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list - -val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference - -val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis - -val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis - -val coerce_to_int_or_var_list : Value.t -> int or_var list - -(** {5 Missing generic arguments} *) - -val wit_constr_context : (Empty.t, Empty.t, constr) genarg_type - -val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 48722f655a..093302608e 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -12,7 +12,6 @@ Equality Contradiction Inv Leminv -Taccoerce Hints Auto Eauto -- cgit v1.2.3 From 82dc377451e2dc7810eea136b9a6ab8fc5ae48b5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Aug 2016 20:34:40 +0200 Subject: Removing dead code in Impargs. --- library/impargs.ml | 3 +-- library/impargs.mli | 12 +----------- 2 files changed, 2 insertions(+), 13 deletions(-) diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e21100..db98bb9fd4 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicits f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt diff --git a/library/impargs.mli b/library/impargs.mli index 34e529ca2c..327f84d9fa 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicits : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) -- cgit v1.2.3 From 553f92462a2bc5e45a0d05c5b051fe51f2e7f2c0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Aug 2016 20:36:32 +0200 Subject: Fix performance bug: do not compute implicits of abstracted lemmas. This was showing up in some of Jason's examples, where an abstract had to compute the weak head form of a huge term in order to find the corresponding implicit arguments. --- tactics/tactics.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 38af9a0caa..ebbd09cb80 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4865,8 +4865,13 @@ let abstract_subproof id gk tac = in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in - (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicits cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in -- cgit v1.2.3 From 219f38188f71bfc665428f2a0f230001cada1e23 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Aug 2016 23:28:41 +0200 Subject: Test file for bug #4187. --- test-suite/bugs/closed/4187.v | 709 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 709 insertions(+) create mode 100644 test-suite/bugs/closed/4187.v diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 0000000000..b13ca36a37 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. -- cgit v1.2.3 From 513e194656429b6a9142a3a34095cee2c6f8ee96 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 20 Aug 2016 10:25:37 +0200 Subject: Fixing an anomaly in printing a unification error message. --- test-suite/success/Case13.v | 8 ++++++++ toplevel/himsg.ml | 1 + 2 files changed, 9 insertions(+) diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8ee..8f95484cfd 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 13a6489b9d..ae6c86c8cc 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -307,6 +307,7 @@ let rec explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e -- cgit v1.2.3 From 1af95525a2a791889e6d72dfc150ff8f09a21e21 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 20 Aug 2016 20:13:28 +0200 Subject: Fixing a bug in the presence of let-in while inferring the return clause. --- pretyping/cases.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487c..fe2b0a5a1a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in -- cgit v1.2.3 From 69a35378d37b8eb7e1019d24ab5e0fd27f25b6bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 20 Aug 2016 21:01:34 +0200 Subject: More standard naming for the Imparg.with_implicits function. --- library/impargs.ml | 2 +- library/impargs.mli | 2 +- tactics/tactics.ml | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/impargs.ml b/library/impargs.ml index db98bb9fd4..bce7a15cbe 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,7 +68,7 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits f x = +let with_implicit_protection f x = let oflags = !implicit_args in try let rslt = f x in diff --git a/library/impargs.mli b/library/impargs.mli index 327f84d9fa..3919a519c9 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,7 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -val with_implicits : ('a -> 'b) -> 'a -> 'b +val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ebbd09cb80..9d08ada60a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4871,7 +4871,7 @@ let abstract_subproof id gk tac = (** ppedrot: seems legit to have abstracted subproofs as local*) Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in - let cst = Impargs.with_implicits cst () in + let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in -- cgit v1.2.3