diff options
Diffstat (limited to 'plugins')
28 files changed, 534 insertions, 191 deletions
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index df4b647642..0cdf8fb5d8 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) } diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8f0440a2a4..c4f8843e51 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d9b19c1ae6..4c24f51b1e 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -58,15 +58,8 @@ let new_entry name = let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode +(* Registers [tactic_mode] as a parser for proof editing *) +let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 1ea6ff84d4..cdee012a82 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -83,7 +83,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 31fb1c9abf..db8d1b20d8 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_morphism_infer atts m n; } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n; } | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts binders m s n; } diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 46ea3819ac..7bf705ffeb 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] ; intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST0 intropattern -> { l } ] ] ; ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] + [ [ l = LIST1 intropattern -> { l } ] ] ; or_and_intropattern: [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } @@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram | "?" -> { IntroAnonymous } | id = ident -> { IntroIdentifier id } ] ] ; - nonsimple_intropattern: + intropattern: [ [ l = simple_intropattern -> { l } | "*" -> { CAst.make ~loc @@ IntroForthcoming true } | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] @@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "eintros"; pl = ne_intropatterns -> { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) } + | IDENT "eintros" -> + { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) } | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) } diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 4bb52f599a..2055b25ff4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n = in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance - (Some (true, CAst.make @@ CRecord [])) + None ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index d4bafe773f..7adae148bd 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -846,7 +846,7 @@ struct match env with | [] -> ([v],n) | e::l -> - if EConstr.eq_constr sigma e v + if EConstr.eq_constr_nounivs sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index c5a09d677e..a964febf9c 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; @@ -468,6 +469,7 @@ Class can_compute_Z (z : Z) := dummy_can_compute_Z : True. Hint Extern 0 (can_compute_Z ?v) => match isZcst v with true => exact I end : typeclass_instances. Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z). +Defined. Lemma R_one_zero: 1%R <> 0%R. discrR. @@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 94a3d40441..695f000cb1 100644 --- a/plugins/omega/PreOmega.v +++ b/plugins/omega/PreOmega.v @@ -12,6 +12,120 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat. Local Open Scope Z_scope. +(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *) + +(** These tactic use the complete specification of [Z.div] and + [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these + functions from the goal without losing information. The + [Z.euclidean_division_equations_cleanup] tactic removes needless + hypotheses, which makes tactics like [nia] run faster. The tactic + [Z.to_euclidean_division_equations] combines the handling of both variants + of division/quotient and modulo/remainder. *) + +Module Z. + Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma div_0_r_ext x y : y = 0 -> x / y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x. + Proof. intro; subst; destruct x; reflexivity. Qed. + Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0. + Proof. intro; subst; destruct x; reflexivity. Qed. + + Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y. + Proof. intros; apply Z.rem_bound_pos; assumption. Qed. + Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y. + Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed. + Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed. + Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0. + Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed. + + Ltac div_mod_to_equations_generalize x y := + pose proof (Z.div_mod x y); + pose proof (Z.mod_pos_bound x y); + pose proof (Z.mod_neg_bound x y); + pose proof (div_0_r_ext x y); + pose proof (mod_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := x / y) in *; + set (r := x mod y) in *; + clearbody q r. + Ltac quot_rem_to_equations_generalize x y := + pose proof (Z.quot_rem' x y); + pose proof (rem_bound_pos_pos x y); + pose proof (rem_bound_pos_neg x y); + pose proof (rem_bound_neg_pos x y); + pose proof (rem_bound_neg_neg x y); + pose proof (quot_0_r_ext x y); + pose proof (rem_0_r_ext x y); + let q := fresh "q" in + let r := fresh "r" in + set (q := Z.quot x y) in *; + set (r := Z.rem x y) in *; + clearbody q r. + + Ltac div_mod_to_equations_step := + match goal with + | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y + | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y + | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y + | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y + end. + Ltac quot_rem_to_equations_step := + match goal with + | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y + end. + Ltac div_mod_to_equations' := repeat div_mod_to_equations_step. + Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step. + Ltac euclidean_division_equations_cleanup := + repeat match goal with + | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) + | [ H : ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?x < ?x -> _ |- _ ] => clear H + | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H') + | [ H : ?T -> _, H' : ~?T |- _ ] => clear H + | [ H : ~?T -> _, H' : ?T |- _ ] => clear H + | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl) + | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H + | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H') + | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H + | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H + | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H + | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H + | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H + | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf))) + | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf)) + | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf)) + | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H + | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H + | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H + end. + Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup. + Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup. + Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup. +End Z. (** * zify: the Z-ification tactic *) @@ -411,6 +525,24 @@ Ltac zify_N_op := | |- context [ Z.of_N (N.mul ?a ?b) ] => pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in * + (* N.div -> Z.div and a positivity hypothesis *) + | H : context [ Z.of_N (N.div ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in * + + (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *) + | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + | |- context [ Z.of_N (N.div ?a ?b) ] => + pose proof (N2Z.is_nonneg (N.modulo a b)); + pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a)); + rewrite (N2Z.inj_rem a b) in * + (* atoms of type N : we add a positivity condition (if not already there) *) | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 1ca6227f25..aa0370b2ac 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z). Proof. exact Z.eq_equiv. Qed. Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z). +Defined. Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops). Proof. diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v index 7958507819..c8d560cfe9 100644 --- a/plugins/setoid_ring/Ncring_tac.v +++ b/plugins/setoid_ring/Ncring_tac.v @@ -27,41 +27,50 @@ Class nth (R:Type) (t:R) (l:list R) (i:nat). Instance Ifind0 (R:Type) (t:R) l : nth t(t::l) 0. +Defined. Instance IfindS (R:Type) (t2 t1:R) l i {_:nth t1 l i} : nth t1 (t2::l) (S i) | 1. +Defined. Class closed (T:Type) (l:list T). Instance Iclosed_nil T : closed (T:=T) nil. +Defined. Instance Iclosed_cons T t (l:list T) {_:closed l} : closed (t::l). +Defined. Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R). Instance reify_zero (R:Type) lvar op `{Ring (T:=R)(ring0:=op)} : reify (ring0:=op)(PEc 0%Z) lvar op. +Defined. Instance reify_one (R:Type) lvar op `{Ring (T:=R)(ring1:=op)} : reify (ring1:=op) (PEc 1%Z) lvar op. +Defined. Instance reifyZ0 (R:Type) lvar `{Ring (T:=R)} : reify (PEc Z0) lvar Z0|11. +Defined. Instance reifyZpos (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zpos p)) lvar (Zpos p)|11. +Defined. Instance reifyZneg (R:Type) lvar (p:positive) `{Ring (T:=R)} : reify (PEc (Zneg p)) lvar (Zneg p)|11. +Defined. Instance reify_add (R:Type) e1 lvar t1 e2 t2 op @@ -69,6 +78,7 @@ Instance reify_add (R:Type) {_:reify (add:=op) e1 lvar t1} {_:reify (add:=op) e2 lvar t2} : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2). +Defined. Instance reify_mul (R:Type) e1 lvar t1 e2 t2 op @@ -76,6 +86,7 @@ Instance reify_mul (R:Type) {_:reify (mul:=op) e1 lvar t1} {_:reify (mul:=op) e2 lvar t2} : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10. +Defined. Instance reify_mul_ext (R:Type) `{Ring R} lvar (z:Z) e2 t2 @@ -83,6 +94,7 @@ Instance reify_mul_ext (R:Type) `{Ring R} {_:reify e2 lvar t2} : reify (PEmul (PEc z) e2) lvar (@multiplication Z _ _ z t2)|9. +Defined. Instance reify_sub (R:Type) e1 lvar t1 e2 t2 op @@ -90,24 +102,28 @@ Instance reify_sub (R:Type) {_:reify (sub:=op) e1 lvar t1} {_:reify (sub:=op) e2 lvar t2} : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2). +Defined. Instance reify_opp (R:Type) e1 lvar t1 op `{Ring (T:=R)(opp:=op)} {_:reify (opp:=op) e1 lvar t1} : reify (opp:=op) (PEopp e1) lvar (op t1). +Defined. Instance reify_pow (R:Type) `{Ring R} e1 lvar t1 n `{Ring (T:=R)} {_:reify e1 lvar t1} : reify (PEpow e1 n) lvar (pow_N t1 n)|1. +Defined. Instance reify_var (R:Type) t lvar i `{nth R t lvar i} `{Rr: Ring (T:=R)} : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t | 100. +Defined. Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) (lterm:list R). @@ -115,12 +131,14 @@ Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) Instance reify_nil (R:Type) lvar `{Rr: Ring (T:=R)} : reifylist (Rr:= Rr) nil lvar (@nil R). +Defined. Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2 `{Rr: Ring (T:=R)} {_:reify (Rr:= Rr) e1 lvar t1} {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2). +Defined. Definition list_reifyl (R:Type) lexpr lvar lterm `{Rr: Ring (T:=R)} diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v index ae91ee1664..df3677e1c3 100644 --- a/plugins/setoid_ring/Rings_Q.v +++ b/plugins/setoid_ring/Rings_Q.v @@ -15,6 +15,7 @@ Require Export Integral_domain. Require Import QArith. Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq). +Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v index 901b36ed3b..fe7558845d 100644 --- a/plugins/setoid_ring/Rings_R.v +++ b/plugins/setoid_ring/Rings_R.v @@ -20,6 +20,7 @@ constructor;red;intros;subst;trivial. Qed. Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)). +Defined. Instance Rri : (Ring (Ro:=Rops)). constructor; diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index dd2c2d0ba4..9ce9250a43 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -67,7 +67,7 @@ type ssrview = ast_closure_term list type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int (* Only [One] forces an introduction, possibly reducing the goal. *) -type anon_iter = +type anon_kind = | One of string option (* name hint *) | Drop | All @@ -76,25 +76,23 @@ type anon_iter = type ssripat = | IPatNoop | IPatId of Id.t - | IPatAnon of anon_iter (* inaccessible name *) -(* TODO | IPatClearMark *) - | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *) - | IPatCase of (* ipats_mod option * *) ssripatss_or_block (* this is not equivalent to /case /[..|..] if there are already multiple goals *) + | IPatAnon of anon_kind (* inaccessible name *) + | IPatDispatch of ssripatss_or_block (* (..|..) *) + | IPatCase of ssripatss_or_block (* [..|..] *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) + | IPatView of ssrview (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list | IPatFastNondep - | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *) and ssripats = ssripat list and ssripatss = ssripats list and ssripatss_or_block = | Block of id_block | Regular of ssripats list -type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats +type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats type ssrhpats_wtransp = bool * ssrhpats (* tac => inpats *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 311d912efd..c3b9bde9b8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -66,7 +66,7 @@ let check_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps) with Not_found -> errorstrm Pp.(str"No assumption is named " ++ Id.print id) -let test_hypname_exists hyps id = +let test_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps); true with Not_found -> false diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 51116ccd75..e642b5e788 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -29,7 +29,7 @@ val allocc : ssrocc val hyp_id : ssrhyp -> Id.t val hyps_ids : ssrhyps -> Id.t list val check_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> unit -val test_hypname_exists : ('a, 'b) Context.Named.pt -> Id.t -> bool +val test_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> bool val check_hyps_uniq : Id.t list -> ssrhyps -> unit val not_section_id : Id.t -> bool val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 257ecd2a85..8c1363020a 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -94,17 +94,23 @@ let basecuttac name c gl = let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) let havetac ist - (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint))) + (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint))) suff namefst gl = let concl = pf_concl gl in + let pats = tclCompileIPats orig_pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let skols, pats = - List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in + List.partition (function IOpAbstractVars _ -> true | _ -> false) pats in let itac_mkabs = introstac skols in - let itac_c = introstac (IPatClear clr :: pats) in + let itac_c, clr = + match clr with + | None -> introstac pats, [] + | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in let binderstac n = - let rec aux = function 0 -> [] | n -> IPatAnon (One None) :: aux (n-1) in + let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) (introstac binders) in let simpltac = introstac simpl in @@ -160,7 +166,7 @@ let havetac ist gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function - | IPatAbstractVars ids -> ids + | IOpAbstractVars ids -> ids | _ -> assert false) skols) in let skols_args = List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in @@ -203,10 +209,12 @@ let destProd_or_LetIn sigma c = | _ -> raise DestKO let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = + let clr0 = Option.default [] clr0 in + let pats = tclCompileIPats pats in let mkabs gen = abs_wgen false (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function - | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats + | _, Some ((x, _), _) -> fun pats -> IOpId (hoi_id x) :: pats | _ -> fun x -> x in let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> @@ -265,7 +273,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = old_cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with - | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, Tacticals.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> @@ -289,6 +297,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = (** The "suffice" tactic *) let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = + let clr = Option.default [] clr in + let pats = tclCompileIPats pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in let c = match Ssrcommon.ssrterm_of_ast_closure_term c with | (a, (b, Some ct)) -> diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 8a05e25504..35e89dbcea 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -22,7 +22,7 @@ val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac val havetac : ist -> bool * - ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) * + ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) * Ssrast.ssripats) * (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) * (bool * Tacinterp.Value.t option list))) -> @@ -35,7 +35,7 @@ val basecuttac : val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> - ((Ssrast.ssrhyps * Ssrast.ssripats) * 'a) * 'b -> + ((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b -> (Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) @@ -50,7 +50,7 @@ val wlogtac : val sufftac : Ssrast.ist -> - (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) * + (((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list) * Ssrast.ssripat list) * (('a * ast_closure_term) * diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index ce81d83661..a8dfd69240 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -19,14 +19,78 @@ open Proofview.Notations open Ssrast +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option (* must clear, may clear *) + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +let rec pr_ipatop = function + | IOpId id -> Names.Id.print id + | IOpDrop -> Pp.str "_" + | IOpTemporay -> Pp.str "+" + | IOpInaccessible None -> Pp.str "?" + | IOpInaccessible (Some s) -> Pp.str ("?«"^s^"»") + | IOpInaccessibleAll -> Pp.str "*" + | IOpAbstractVars l -> Pp.str ("[:"^String.concat " " (List.map Names.Id.to_string l)^"]") + | IOpFastNondep -> Pp.str ">" + + | IOpInj l -> Pp.(str "[=" ++ ppl l ++ str "]") + + | IOpDispatchBlock b -> Pp.(str"(" ++ Ssrprinters.pr_block b ++ str")") + | IOpDispatchBranches l -> Pp.(str "(" ++ ppl l ++ str ")") + + | IOpCaseBlock b -> Pp.(str"[" ++ Ssrprinters.pr_block b ++ str"]") + | IOpCaseBranches l -> Pp.(str "[" ++ ppl l ++ str "]") + + | IOpRewrite (occ,dir) -> Pp.(Ssrprinters.(pr_occ occ ++ pr_dir dir)) + | IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + | IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + + | IOpClear (clmust,clmay) -> + Pp.(Ssrprinters.pr_clear spc clmust ++ + match clmay with + | Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")" + | None -> mt ()) + | IOpSimpl s -> Ssrprinters.pr_simpl s + + | IOpEqGen _ -> Pp.str "E:" + | IOpNoop -> Pp.str"-" +and ppl x = Pp.(prlist_with_sep (fun () -> str"|") (prlist_with_sep spc pr_ipatop)) x + + module IpatMachine : sig (* the => tactical. ?eqtac is a tactic to be eventually run * after the first [..] block. first_case_is_dispatch is the * ssr exception to elim: and case: *) val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool -> - ssripats -> unit tactic + ssriops -> unit tactic + val tclCompileIPats : ssripats -> ssriops val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic @@ -53,7 +117,7 @@ module State : sig val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic (* Some data may expire *) - val isTICK : ssripat -> unit tactic + val isTICK : ssriop -> unit tactic val isPRINT : Proofview.Goal.t -> Pp.t @@ -149,7 +213,7 @@ let isNSEED_CONSUME k = k x) let isTICK = function - | IPatSimpl _ | IPatClear _ -> tclUNIT () + | IOpSimpl _ | IOpClear _ -> tclUNIT () | _ -> tclGET (fun s -> tclSET { s with name_seed = None }) end (* }}} *************************************************************** *) @@ -238,6 +302,13 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl -> tclUNIT () end +let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl -> + let ctx = Goal.hyps gl in + k (Option.bind hyps (fun h -> + if Ssrcommon.test_hyp_exists ctx h && + Ssrcommon.(not_section_id (hyp_id h)) then Some h else None)) +end + (** [=> []] *****************************************************************) (* calls t1 then t2 on each subgoal passing to t2 the index of the current @@ -286,13 +357,13 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> | Prefix id -> Id.to_string id ^ "?" | SuffixNum n -> "?" ^ string_of_int n | SuffixId id -> "?" ^ Id.to_string id in - IPatAnon (One (Some s)) + IOpInaccessible (Some s) | Name id -> let s = match fix with | Prefix fix -> Id.to_string fix ^ Id.to_string id | SuffixNum n -> Id.to_string id ^ string_of_int n | SuffixId fix -> Id.to_string id ^ Id.to_string fix in - IPatId (Id.of_string s)) seeds in + IOpId (Id.of_string s)) seeds in interp_ipats ipats end end @@ -342,7 +413,7 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p)); + Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> @@ -362,58 +433,74 @@ let tclLOG p t = let notTAC = tclUNIT false +let duplicate_clear = + CWarnings.create ~name:"duplicate-clear" ~category:"ssr" + (fun id -> Pp.(str "Duplicate clear of " ++ Id.print id)) + (* returns true if it was a tactic (eg /ltac:tactic) *) let rec ipat_tac1 ipat : bool tactic = match ipat with - | IPatView (clear_if_id,l) -> + | IOpView (glued_clear,l) -> + let clear_if_id, extra_clear = + match glued_clear with + | None -> false, [] + | Some x -> true, List.map Ssrcommon.hyp_id x in Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id - ~conclusion:(fun ~to_clear:clr -> intro_clear clr) + ~conclusion:(fun ~to_clear:clr -> + let inter = CList.intersect Id.equal clr extra_clear in + List.iter duplicate_clear inter; + let cl = CList.union Id.equal clr extra_clear in + intro_clear cl) - | IPatDispatch(true, Regular [[]]) -> - notTAC - | IPatDispatch(_, Regular ipatss) -> + | IOpDispatchBranches ipatss -> tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC - | IPatDispatch(_,Block id_block) -> + | IOpDispatchBlock id_block -> tac_intro_seed ipat_tac id_block <*> notTAC - - | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC - | IPatFastNondep -> intro_anon_deps <*> notTAC - - | IPatCase (Block id_block) -> + | IOpCaseBlock id_block -> Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC - | IPatCase (Regular ipatss) -> + | IOpCaseBranches ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC - | IPatInj ipatss -> + + | IOpId id -> Ssrcommon.tclINTRO_ID id <*> notTAC + | IOpFastNondep -> intro_anon_deps <*> notTAC + | IOpDrop -> intro_drop <*> notTAC + | IOpInaccessible seed -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC + | IOpInaccessibleAll -> intro_anon_all <*> notTAC + | IOpTemporay -> intro_anon_temp <*> notTAC + + | IOpSimpl Nop -> assert false + + | IOpInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss <*> notTAC - | IPatAnon Drop -> intro_drop <*> notTAC - | IPatAnon (One seed) -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC - | IPatAnon All -> intro_anon_all <*> notTAC - | IPatAnon Temporary -> intro_anon_temp <*> notTAC - - | IPatNoop -> notTAC - | IPatSimpl Nop -> notTAC - - | IPatClear ids -> - tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) <*> + | IOpClear (must,may) -> + tacCHECK_HYPS_EXIST must <*> + tacFILTER_HYP_EXIST may (fun may -> + let must = List.map Ssrcommon.hyp_id must in + let cl = Option.fold_left (fun cls (SsrHyp(_,id)) -> + if CList.mem_f Id.equal id cls then begin + duplicate_clear id; + cls + end else id :: cls) must may in + intro_clear cl) <*> notTAC - | IPatSimpl x -> + | IOpSimpl x -> V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC - | IPatRewrite (occ,dir) -> + | IOpRewrite (occ,dir) -> Ssrcommon.tclWITHTOP (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC - | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC + | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC - | IPatEqGen t -> t <*> notTAC + | IOpEqGen t -> t <*> notTAC + | IOpNoop -> notTAC and ipat_tac pl : unit tactic = match pl with @@ -433,51 +520,88 @@ and tclIORPAT tac = function | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) and ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) + | Some (IOpCaseBranches [[]]) when is_on -> Some IOpNoop + | Some (IOpCaseBranches l) when is_on -> + Some (IOpDispatchBranches l) + | Some (IOpCaseBlock s) when is_on -> + Some (IOpDispatchBlock s) | x -> x and option_to_list = function None -> [] | Some x -> [x] and split_at_first_case ipats = let rec loop acc = function - | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest - | (IPatCase _ | IPatDispatch _) as x :: xs -> CList.rev acc, Some x, xs + | (IOpSimpl _ | IOpClear _) as x :: rest -> loop (x :: acc) rest + | (IOpCaseBlock _ | IOpCaseBranches _ + | IOpDispatchBlock _ | IOpDispatchBranches _) as x :: xs -> + CList.rev acc, Some x, xs | pats -> CList.rev acc, None, pats in loop [] ipats ;; (* Simple pass doing {x}/v -> /v{x} *) -let elaborate_ipats l = +let tclCompileIPats l = let rec elab = function + + | (IPatClear cl) :: (IPatView v) :: rest -> + (IOpView(Some cl,v)) :: elab rest + | (IPatClear cl) :: (IPatId id) :: rest -> + (IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest + + (* boring code *) | [] -> [] - | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest - | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest - | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest - | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest - | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep | - IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | - IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest - in - elab l -let main ?eqtac ~first_case_is_dispatch ipats = - let ipats = elaborate_ipats ipats in - let ip_before, case, ip_after = split_at_first_case ipats in + | IPatId id :: rest -> IOpId id :: elab rest + | IPatAnon (One hint) ::rest -> IOpInaccessible hint :: elab rest + | IPatAnon Drop :: rest -> IOpDrop :: elab rest + | IPatAnon All :: rest -> IOpInaccessibleAll :: elab rest + | IPatAnon Temporary :: rest -> IOpTemporay :: elab rest + | IPatAbstractVars vs :: rest -> IOpAbstractVars vs :: elab rest + | IPatFastNondep :: rest -> IOpFastNondep :: elab rest + + | IPatInj pats :: rest -> IOpInj (List.map elab pats) :: elab rest + | IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest + | IPatView vs :: rest -> IOpView (None,vs) :: elab rest + | IPatSimpl s :: rest -> IOpSimpl s :: elab rest + | IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest + + | IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest + | IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest + | IPatDispatch (Block seed) :: rest -> IOpDispatchBlock seed :: elab rest + | IPatDispatch (Regular bs) :: rest -> IOpDispatchBranches (List.map elab bs) :: elab rest + | IPatNoop :: rest -> IOpNoop :: elab rest + + in + elab l +;; +let tclCompileIPats l = + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + prlist_with_sep spc Ssrprinters.pr_ipat l)); + let ops = tclCompileIPats l in + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + prlist_with_sep spc pr_ipatop ops)); + ops + +let main ?eqtac ~first_case_is_dispatch iops = + let ip_before, case, ip_after = split_at_first_case iops in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in - let eqtac = option_to_list (Option.map (fun x -> IPatEqGen x) eqtac) in - Ssrcommon.tcl0G ~default:() (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + let eqtac = option_to_list (Option.map (fun x -> IOpEqGen x) eqtac) in + let ipats = ip_before @ case @ eqtac @ ip_after in + Ssrcommon.tcl0G ~default:() (ipat_tac ipats <*> intro_end) end (* }}} *) let tclIPAT_EQ eqtac ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~eqtac ~first_case_is_dispatch:true ip + IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~first_case_is_dispatch:true ip + IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) + +let tclCompileIPats = IpatMachine.tclCompileIPats (* Common code to handle generalization lists along with the defective case *) let with_defective maintac deps clr = Goal.enter begin fun g -> @@ -721,12 +845,12 @@ let eqmovetac _ gen = ;; let rec eqmoveipats eqpat = function - | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> + | (IOpSimpl _ | IOpClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats - | (IPatAnon All :: _ | []) as ipats -> - IPatAnon (One None) :: eqpat :: ipats + | (IOpInaccessibleAll :: _ | []) as ipats -> + IOpInaccessible None :: eqpat @ ipats | ipat :: ipats -> - ipat :: eqpat :: ipats + ipat :: eqpat @ ipats let ssrsmovetac = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in @@ -736,7 +860,6 @@ let ssrsmovetac = Goal.enter begin fun g -> end let tclIPAT ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.main ~first_case_is_dispatch:false ip let ssrmovetac = function @@ -748,17 +871,17 @@ let ssrmovetac = function gentac <*> tclLAST_GEN ~to_ind:false lastgen (tacVIEW_THEN_GRAB view ~conclusion) <*> - tclIPAT (IPatClear clr :: ipats) + tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) + tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in - dgentac <*> tclIPAT (eqmoveipats pat ipats) + dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats)) | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in - gentac <*> tclIPAT ipats + gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats) | _, (_, ({ clr }, ipats)) -> - Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats] + Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)] (** [abstract: absvar gens] **************************************************) let rec is_Evar_or_CastedMeta sigma x = diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 89cba4be71..893061b154 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -19,8 +19,44 @@ open Ssrast +(* Atomic operations for the IPat machine. Use this if you are "patching" an + * ipat written by the user, since patching it at he AST level and then + * compiling it may have tricky effects, eg adding a clear in front of a view + * also has the effect of disposing the view (the compilation phase takes care + * of this, by using the compiled ipats you can be more precise *) +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +val tclCompileIPats : ssripats -> ssriops + (* The => tactical *) -val tclIPAT : ssripats -> unit Proofview.tactic +val tclIPAT : ssriops -> unit Proofview.tactic (* As above but with the SSR exception: first case is dispatch *) val tclIPATssr : ssripats -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 76726009ac..3fb21e5ef6 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -635,11 +635,10 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat)) - | IPatDispatch (s, Regular iorpat) -> IPatDispatch (s, Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) - | IPatDispatch (s, Block (hat)) -> IPatDispatch (s, Block(map_block map_id hat)) + | IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) + | IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat)) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) - | IPatEqGen _ -> assert false (*internal usage only *) + | IPatView v -> IPatView (List.map map_ast_closure_term v) and map_block map_id = function | Prefix id -> Prefix (map_id id) | SuffixId id -> SuffixId (map_id id) @@ -715,22 +714,22 @@ let interp_ipat ist gl = if not (ltacvar id) then hyp :: hyps else add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in - check_hyps_uniq [] clr'; IPatClear clr' + check_hyps_uniq [] clr'; + IPatClear clr' | IPatCase(Regular iorpat) -> IPatCase(Regular(List.map (List.map interp) iorpat)) | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat)) - | IPatDispatch(s,Regular iorpat) -> - IPatDispatch(s,Regular (List.map (List.map interp) iorpat)) - | IPatDispatch(s,Block(hat)) -> IPatDispatch(s,Block(interp_block hat)) + | IPatDispatch(Regular iorpat) -> + IPatDispatch(Regular (List.map (List.map interp) iorpat)) + | IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat)) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x - | IPatEqGen _ -> assert false (*internal usage only *) in interp @@ -765,10 +764,6 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] } - | [ ssrdocc(occ) ssrfwdview(v) ] -> { match occ with - | Some [], _ -> [IPatView (true,v)] - | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] - | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } | [ ssrdocc(occ) ] -> { match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } @@ -786,7 +781,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] } | [ "-/" integer(n) "/" integer (m) "=" ] -> { [IPatNoop;IPatSimpl(SimplCut(n,m))] } - | [ ssrfwdview(v) ] -> { [IPatView (false,v)] } + | [ ssrfwdview(v) ] -> { [IPatView v] } | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } END @@ -875,11 +870,12 @@ ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats } let check_ssrhpats loc w_binders ipats = let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in let clr, ipats = + let opt_app = function None -> fun l -> Some l + | Some l1 -> fun l2 -> Some (l1 @ l2) in let rec aux clr = function - | IPatClear cl :: tl -> aux (clr @ cl) tl -(* | IPatSimpl (cl, sim) :: tl -> clr @ cl, IPatSimpl ([], sim) :: tl *) + | IPatClear cl :: tl -> aux (opt_app clr cl) tl | tl -> clr, tl - in aux [] ipats in + in aux None ipats in let simpl, ipats = match List.rev ipats with | IPatSimpl _ as s :: tl -> [s], List.rev tl @@ -903,27 +899,29 @@ let check_ssrhpats loc w_binders ipats = in loop [] ipats in ((clr, ipat), binders), simpl +let pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x + let pr_hpats (((clr, ipat), binders), simpl) = - pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl + pr_clear_opt mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl let pr_ssrhpats _ _ _ = pr_hpats let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x } -ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear * ssripat) * ssripat) * ssripat) +ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear option * ssripat) * ssripat) * ssripat) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc true i } END ARGUMENT EXTEND ssrhpats_wtransp - TYPED AS (bool * (((ssrclear * ssripats) * ssripats) * ssripats)) + TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats)) PRINTED BY { pr_ssrhpats_wtransp } | [ ssripats(i) ] -> { false,check_ssrhpats loc true i } | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) } END ARGUMENT EXTEND ssrhpats_nobs -TYPED AS (((ssrclear * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } +TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc false i } END @@ -2051,7 +2049,7 @@ END (* We just add a numeric version that clears the n top assumptions. *) TACTIC EXTEND ssrclear - | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IPatAnon Drop)) } + | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IOpDrop)) } END (** The "move" tactic *) @@ -2090,10 +2088,10 @@ let movearg_of_parsed_movearg (v,(eq,(dg,ip))) = TACTIC EXTEND ssrmove | [ "move" ssrmovearg(arg) ssrrpat(pat) ] -> - { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] } + { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT (tclCompileIPats [pat]) } | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] -> { tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses } -| [ "move" ssrrpat(pat) ] -> { tclIPAT [pat] } +| [ "move" ssrrpat(pat) ] -> { tclIPAT (tclCompileIPats [pat]) } | [ "move" ] -> { ssrsmovetac } END @@ -2632,7 +2630,11 @@ END { -let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z) +let augment_preclr clr1 (((clr0, x),y),z) = + let cl = match clr0 with + | None -> if clr1 = [] then None else Some clr1 + | Some clr0 -> Some (clr1 @ clr0) in + (((cl, x),y),z) } diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 898e03b00e..38f5b7d107 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -74,7 +74,7 @@ let pr_occ = function | None -> str "{}" let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}" -let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr +let pr_clear sep clr = sep () ++ pr_clear_ne clr let pr_dir = function L2R -> str "->" | R2L -> str "<-" @@ -102,20 +102,18 @@ let rec pr_ipat p = | IPatClear clr -> pr_clear mt clr | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") | IPatCase (Block m) -> hov 1 (str"[" ++ pr_block m ++ str"]") - | IPatDispatch(_,Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") - | IPatDispatch (_,Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") + | IPatDispatch(Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") + | IPatDispatch (Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon (One _) -> str "?" - | IPatView (false,v) -> pr_view2 v - | IPatView (true,v) -> str"{}" ++ pr_view2 v + | IPatView v -> pr_view2 v | IPatAnon Temporary -> str "+" | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatFastNondep -> str">" - | IPatEqGen _ -> str "<tac>" and pr_ipats ipats = pr_list spc pr_ipat ipats and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat and pr_block = function (Prefix id) -> str"^" ++ Id.print id diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 31c360ad6d..5f20ac2705 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -43,6 +43,7 @@ val pr_view2 : ast_closure_term list -> Pp.t val pr_ipat : ssripat -> Pp.t val pr_ipats : ssripats -> Pp.t val pr_iorpat : ssripatss -> Pp.t +val pr_block : id_block -> Pp.t val pr_hyp : ssrhyp -> Pp.t val pr_hyps : ssrhyps -> Pp.t diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 4816027296..2794696017 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -142,7 +142,7 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce = To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we need to internalize t. *) -let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = +let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } = Goal.(enter_one ~__LOC__ begin fun goal -> let genv = env goal in let sigma = sigma goal in @@ -161,7 +161,7 @@ let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = | Glob_term.GHole (_,_, Some x) when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic) -> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x)) - | _ -> tclUNIT (`Term (interp_env, g)) + | _ -> tclUNIT (`Term (annotation, interp_env, g)) end) (* To inject a constr into a glob_constr we use an Ltac variable *) @@ -207,7 +207,7 @@ let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = Ssrprinters.ppdebug (lazy Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); - let hd, _ = EConstr.decompose_app ist t in + let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) | _ -> tclUNIT (x,[]) @@ -280,8 +280,9 @@ let interp_view ~clear_if_id ist v p = else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view ~clear_if_id (ist, v) = +let pile_up_view ~clear_if_id (annotation, ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in + let clear_if_id = clear_if_id && annotation <> `Parens in State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index f0bb6f58a6..ff2c900130 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -1,5 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) open Goal open Environ diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 9a53e1dd1a..a39f76db9e 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -1,5 +1,15 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + (* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) + Declare ML Module "ssrmatching_plugin". Module SsrMatchingSyntax. diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 470deb4a60..ea564ae2ba 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -33,30 +33,41 @@ let get_constructors ind = Array.to_list (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) -let q_z = qualid_of_string "Coq.Numbers.BinNums.Z" -let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive" -let q_int = qualid_of_string "Coq.Init.Decimal.int" -let q_uint = qualid_of_string "Coq.Init.Decimal.uint" -let q_option = qualid_of_string "Coq.Init.Datatypes.option" +let qualid_of_ref n = + n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty + +let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with | IndRef i -> i | _ -> raise Not_found -let locate_ind q = - try unsafe_locate_ind q - with Not_found -> Nametab.error_global_not_found q - let locate_z () = - try - Some { z_ty = unsafe_locate_ind q_z; - pos_ty = unsafe_locate_ind q_positive } - with Not_found -> None + let zn = "num.Z.type" in + let pn = "num.pos.type" in + if Coqlib.has_ref zn && Coqlib.has_ref pn + then + let q_z = qualid_of_ref zn in + let q_pos = qualid_of_ref pn in + Some ({ + z_ty = unsafe_locate_ind q_z; + pos_ty = unsafe_locate_ind q_pos; + }, mkRefC q_z) + else None let locate_int () = - { uint = locate_ind q_uint; - int = locate_ind q_int } + let int = "num.int.type" in + let uint = "num.uint.type" in + if Coqlib.has_ref int && Coqlib.has_ref uint + then + let q_int = qualid_of_ref int in + let q_uint = qualid_of_ref uint in + Some ({ + int = unsafe_locate_ind q_int; + uint = unsafe_locate_ind q_uint; + }, mkRefC q_int, mkRefC q_uint) + else None let has_type f ty = let (sigma, env) = Pfedit.get_current_context () in @@ -64,19 +75,17 @@ let has_type f ty = try let _ = Constrintern.interp_constr env sigma c in true with Pretype_errors.PretypeError _ -> false -let type_error_to f ty loadZ = +let type_error_to f ty = CErrors.user_err (pr_qualid f ++ str " should go from Decimal.int to " ++ pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) + fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).") -let type_error_of g ty loadZ = +let type_error_of g ty = CErrors.user_err (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ - str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++ - (if loadZ then str " (require BinNums first)." else str ".")) + str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).") let vernac_numeral_notation local ty f g scope opts = let int_ty = locate_int () in @@ -86,43 +95,36 @@ let vernac_numeral_notation local ty f g scope opts = let of_ty = Smartlocate.global_with_alias g in let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in - let cref q = mkRefC q in let arrow x y = mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) in - let cZ = cref q_z in - let cint = cref q_int in - let cuint = cref q_uint in - let coption = cref q_option in - let opt r = app coption r in + let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = - if has_type f (arrow cint cty) then Int int_ty, Direct - else if has_type f (arrow cint (opt cty)) then Int int_ty, Option - else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct - else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type f (arrow cZ cty) then Z z_pos_ty, Direct - else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option - else type_error_to f ty false - | None -> type_error_to f ty true + match int_ty with + | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option + | _ -> type_error_to f ty in (* Check the type of g *) let of_kind = - if has_type g (arrow cty cint) then Int int_ty, Direct - else if has_type g (arrow cty (opt cint)) then Int int_ty, Option - else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct - else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option - else - match z_pos_ty with - | Some z_pos_ty -> - if has_type g (arrow cty cZ) then Z z_pos_ty, Direct - else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option - else type_error_of g ty false - | None -> type_error_of g ty true + match int_ty with + | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct + | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option + | _ -> type_error_of g ty in let o = { to_kind; to_ty; of_kind; of_ty; ty_name = ty; |