diff options
Diffstat (limited to 'plugins')
33 files changed, 222 insertions, 204 deletions
diff --git a/plugins/cc/g_congruence.mlg b/plugins/cc/g_congruence.mlg index 3920e3da75..2c91901477 100644 --- a/plugins/cc/g_congruence.mlg +++ b/plugins/cc/g_congruence.mlg @@ -22,9 +22,9 @@ DECLARE PLUGIN "cc_plugin" TACTIC EXTEND cc | [ "congruence" ] -> { congruence_tac 1000 [] } -| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" natural(n) ] -> { congruence_tac n [] } | [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } - |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> +| [ "congruence" natural(n) "with" ne_constr_list(l) ] -> { congruence_tac n l } END diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg index 094f87f154..da7ed7be64 100644 --- a/plugins/extraction/g_extraction.mlg +++ b/plugins/extraction/g_extraction.mlg @@ -60,16 +60,10 @@ let pr_language = function | Scheme -> str "Scheme" | JSON -> str "JSON" -let warn_deprecated_ocaml_spelling = - CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated" - (fun () -> - strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\".")) - } VERNAC ARGUMENT EXTEND language PRINTED BY { pr_language } -| [ "Ocaml" ] -> { let _ = warn_deprecated_ocaml_spelling () in Ocaml } | [ "OCaml" ] -> { Ocaml } | [ "Haskell" ] -> { Haskell } | [ "Scheme" ] -> { Scheme } diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg index cb226de586..f1f538ab39 100644 --- a/plugins/ltac/coretactics.mlg +++ b/plugins/ltac/coretactics.mlg @@ -263,7 +263,7 @@ END (** Double induction *) -TACTIC EXTEND double_induction +TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () } | [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> { Elim.h_double_induction h1 h2 } END diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index eb53fd45d0..863c4d37d8 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -25,7 +25,7 @@ open Locus (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *) let create_generic_quotation name e wit = - let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in + let inject (loc, v) = Tacexpr.TacGeneric (Some name, Genarg.in_gen (Genarg.rawwit wit) v) in Tacentries.create_ltac_quotation name inject (e, None) let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 66c72a30a2..4f20e5a800 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin" (**********************************************************************) (* replace, discriminate, injection, simplify_eq *) -(* cutrewrite, dependent rewrite *) +(* dependent rewrite *) let with_delayed_uconstr ist c tac = let flags = { @@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite -> { rewriteInHyp b c id } END -TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } -| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> { cutRewriteInHyp b eqn id } -END - (**********************************************************************) (* Decompose *) diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 35c90444b1..8d197e6056 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -77,7 +77,7 @@ END (* true = All transparent, false = Opaque if possible *) VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> { set_typeclasses_debug d; Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 114acaa412..d88cda177e 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -180,7 +180,7 @@ GRAMMAR EXTEND Gram [ [ a = tactic_arg -> { a } | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } (* Unambiguous entries: tolerated w/o "ltac:" modifier *) - | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) tactic_arg: @@ -209,9 +209,9 @@ GRAMMAR EXTEND Gram | c = Constr.constr -> { ConstrTerm c } ] ] ; tactic_atom: - [ [ n = integer -> { TacGeneric (genarg_of_int n) } + [ [ n = integer -> { TacGeneric (None, genarg_of_int n) } | r = reference -> { TacCall (CAst.make ~loc (r,[])) } - | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ] ; match_key: [ [ "match" -> { Once } @@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram message_token: [ [ id = identref -> { MsgIdent id } | s = STRING -> { MsgString s } - | n = integer -> { MsgInt n } ] ] + | n = natural -> { MsgInt n } ] ] ; ltac_def_kind: diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index fa176482bf..a6673699af 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[])) } VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> { obligation (num, Some name, Some t) tac } -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> +| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] -> { obligation (num, Some name, None) tac } -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> +| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] -> { obligation (num, None, Some t) tac } -| [ "Obligation" integer(num) withtac(tac) ] -> +| [ "Obligation" natural(num) withtac(tac) ] -> { obligation (num, None, None) tac } | [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> { next_obligation (Some name) tac } @@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_ END VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> +| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] -> { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> +| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] -> { try_solve_obligation num None (Some (Tacinterp.interp t)) } END diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 0024d1a4ba..47df3ec34f 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -228,14 +228,15 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let c = fill_holes pfterm in (* warning: side-effect on ownSign *) let invProof = it_mkNamedLambda_or_LetIn c !ownSign in - let p = EConstr.to_constr sigma invProof in - p, sigma + invProof, sigma let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in - let univs = Evd.univ_entry ~poly sigma in - let entry = Declare.definition_entry ~univs invProof in - let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in + let cinfo = Declare.CInfo.make ~name ~typ:None () in + let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in + let _ : Names.GlobRef.t = + Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma + in () (* inv_op = Inv (derives de complete inv. lemma) @@ -246,11 +247,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in - try - add_inversion_lemma ~poly na env sigma c sort bool tac - with - | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) - user_err ~hdr:"Inv needs Nodep Prop Set" s + add_inversion_lemma ~poly na env sigma c sort bool tac (* ================================= *) (* Applying a given inversion lemma *) diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6233807016..85bb901046 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -338,8 +338,8 @@ let string_of_genarg_arg (ArgumentType arg) = | Extend.Uentryl (_, l) -> prtac LevelSome arg | _ -> match arg with - | TacGeneric arg -> - let pr l arg = prtac l (TacGeneric arg) in + | TacGeneric (isquot,arg) -> + let pr l arg = prtac l (TacGeneric (isquot,arg)) in pr_any_arg pr symb arg | _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")" @@ -571,7 +571,7 @@ let pr_goal_selector ~toplevel s = let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = let pr = function - | TacGeneric arg -> + | TacGeneric (_,arg) -> let name = string_of_genarg_arg (genarg_tag arg) in if name = "unit" || name = "int" then (* Hard-wired parsing rules *) @@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s = ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h ) | TacChange (check,op,c,h) -> - let name = if check then "change_no_check" else "change" in + let name = if check then "change" else "change_no_check" in hov 1 ( primitive name ++ brk (1,1) ++ ( @@ -1049,8 +1049,9 @@ let pr_goal_selector ~toplevel s = pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval | TacArg { CAst.v=TacFreshId l } -> primitive "fresh" ++ pr_fresh_ids l, latom - | TacArg { CAst.v=TacGeneric arg } -> - pr.pr_generic env sigma arg, latom + | TacArg { CAst.v=TacGeneric (isquot,arg) } -> + let p = pr.pr_generic env sigma arg in + (match isquot with Some name -> str name ++ str ":(" ++ p ++ str ")" | None -> p), latom | TacArg { CAst.v=TacCall {CAst.v=(f,[])} } -> pr.pr_reference f, latom | TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } -> diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg index eb9d9cbdce..e5309ea441 100644 --- a/plugins/ltac/profile_ltac_tactics.mlg +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -55,7 +55,7 @@ END TACTIC EXTEND show_ltac_profile | [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } | [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } END @@ -74,7 +74,7 @@ END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY | [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } +| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) } END VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index fb149071c9..a1dbf9a439 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -546,7 +546,7 @@ let rewrite_core_unif_flags = { Unification.check_applied_meta_types = true; Unification.use_pattern_unification = true; Unification.use_meta_bound_pattern_unification = true; - Unification.allowed_evars = Unification.AllowAll; + Unification.allowed_evars = Evarsolve.AllowedEvars.all; Unification.restrict_conv_on_strict_subterms = false; Unification.modulo_betaiota = false; Unification.modulo_eta = true; diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 91d26519b8..f7037176d2 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -394,7 +394,7 @@ type appl = (* Values for interpretation *) type tacvalue = - | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t * Name.t list * Tacexpr.glob_tactic_expr | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 3afbb56b23..b8592c5c76 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -104,7 +104,7 @@ type appl = (** For calls to global constants, some may alias other. *) type tacvalue = - | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t * + | VFun of appl *Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t * Name.t list * Tacexpr.glob_tactic_expr | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index f8c25d5dd0..fcd60ea250 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -174,7 +174,7 @@ let add_tactic_entry (kn, ml, tg) state = if Genarg.has_type arg wit && not ml then Tacexp (Genarg.out_gen wit arg) else - TacGeneric arg + TacGeneric (None, arg) in let l = List.map map l in (TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr) @@ -349,7 +349,7 @@ let extend_atomic_tactic name entries = | TacNonTerm (_, (symb, _)) -> let EntryName (typ, e) = prod_item_of_symbol 0 symb in let Genarg.Rawwit wit = typ in - let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in + let inj x = TacArg (CAst.make @@ TacGeneric (None, Genarg.in_gen typ x)) in let default = epsilon_value inj e in match default with | None -> raise NonEmptyArgument @@ -780,7 +780,7 @@ let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac = let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in let len = ml_sig_len sign in let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in - let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in + let body = TacGeneric (None, in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in let vars = List.map (fun id -> Name id) vars in let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in let id = Names.Id.of_string name in @@ -876,7 +876,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = let (rpr, gpr, tpr) = arg.arg_printer in let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in let () = create_ltac_quotation name - (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v)) + (fun (loc, v) -> Tacexpr.TacGeneric (Some name,Genarg.in_gen (Genarg.rawwit wit) v)) (entry, None) in (wit, entry) diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index b261096b63..eaedf8d9c1 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -154,7 +154,7 @@ constraint 'a = < (** Possible arguments of a tactic definition *) type 'a gen_tactic_arg = - | TacGeneric of 'lev generic_argument + | TacGeneric of string option * 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 650349b586..50767821e4 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -153,7 +153,7 @@ constraint 'a = < (** Possible arguments of a tactic definition *) type 'a gen_tactic_arg = - | TacGeneric of 'lev generic_argument + | TacGeneric of string option * 'lev generic_argument | ConstrMayEval of ('trm,'cst,'pat) may_eval | Reference of 'ref | TacCall of ('ref * 'a gen_tactic_arg list) CAst.t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index afa79a88db..dea216045e 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -195,7 +195,7 @@ let intern_non_tactic_reference strict ist qid = if qualid_is_ident qid && not strict then let id = qualid_basename qid in let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in - TacGeneric ipat + TacGeneric (None,ipat) else (* Reference not found *) let _, info = Exninfo.capture exn in @@ -713,9 +713,9 @@ and intern_tacarg strict onlytac ist = function | TacPretype c -> TacPretype (intern_constr ist c) | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (intern_tactic onlytac ist t) - | TacGeneric arg -> + | TacGeneric (isquot,arg) -> let arg = intern_genarg ist arg in - TacGeneric arg + TacGeneric (isquot,arg) (* Reads the rules of a Match Context or a Match *) and intern_match_rule onlytac ist ?(as_type=false) = function diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 88480194c8..ff6a36a049 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -124,7 +124,7 @@ let is_traced () = let name_vfun appl vle = if is_traced () && has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with - | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t)) + | VFun (appl0,trace,loc,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t)) | _ -> vle else vle @@ -134,6 +134,7 @@ let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field () (* ids inherited from the call context (needed to get fresh ids) *) let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () +let f_loc : Loc.t TacStore.field = TacStore.field () (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = Geninterp.interp_sign = @@ -141,12 +142,23 @@ type interp_sign = Geninterp.interp_sign = ; poly : bool ; extra : TacStore.t } +let add_extra_trace trace extra = TacStore.set extra f_trace trace let extract_trace ist = if is_traced () then match TacStore.get ist.extra f_trace with | None -> [] | Some l -> l else [] +let add_extra_loc loc extra = + match loc with + | None -> extra + | Some loc -> TacStore.set extra f_loc loc +let add_loc loc ist = + match loc with + | None -> ist + | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc } +let extract_loc ist = TacStore.get ist.extra f_loc + let print_top_val env v = Pptactic.pr_value Pptactic.ltop v let catching_error call_trace fail (e, info) = @@ -222,7 +234,7 @@ let pr_inspect env expr result = let pp_result = if has_type result (topwit wit_tacvalue) then match to_tacvalue result with - | VFun (_,_, ist, ul, b) -> + | VFun (_, _, _, ist, ul, b) -> let body = if List.is_empty ul then b else (TacFun (ul, b)) in str "a closure with body " ++ fnl() ++ pr_closure env ist body | VRec (ist, body) -> @@ -249,10 +261,10 @@ let propagate_trace ist loc id v = if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with - | VFun (appl,_,lfun,it,b) -> + | VFun (appl,_,_,lfun,it,b) -> let t = if List.is_empty it then b else TacFun (it,b) in let trace = push_trace(loc,LtacVarCall (id,t)) ist in - let ans = VFun (appl,trace,lfun,it,b) in + let ans = VFun (appl,trace,loc,lfun,it,b) in Proofview.tclUNIT (of_tacvalue ans) | _ -> Proofview.tclUNIT v else Proofview.tclUNIT v @@ -260,7 +272,7 @@ let propagate_trace ist loc id v = let append_trace trace v = if has_type v (topwit wit_tacvalue) then match to_tacvalue v with - | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b)) + | VFun (appl,trace',loc,lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,loc,lfun,it,b)) | _ -> v else v @@ -272,7 +284,7 @@ let coerce_to_tactic loc id v = if has_type v (topwit wit_tacvalue) then let tacv = to_tacvalue v in match tacv with - | VFun _ -> v + | VFun (appl,trace,_,lfun,it,b) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b)) | _ -> fail () else fail () @@ -1062,7 +1074,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti function. *) let value_interp ist = match tac with | TacFun (it, body) -> - Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, it, body))) + Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body))) | TacLetIn (true,l,u) -> interp_letrec ist l u | TacLetIn (false,l,u) -> interp_letin ist l u | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr @@ -1070,7 +1082,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti | TacArg {loc;v} -> interp_tacarg ist v | t -> (* Delayed evaluation *) - Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t))) + Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], t))) in let open Ftactic in Control.check_for_interrupt (); @@ -1163,7 +1175,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) - | TacArg a -> Ftactic.run (val_interp ist tac) (fun v -> catch_error_loc a.CAst.loc false (tactic_of_value ist v)) + | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v) | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> @@ -1178,9 +1190,9 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with let ist = { lfun ; poly - ; extra = TacStore.set ist.extra f_trace trace } in + ; extra = add_extra_loc loc (add_extra_trace trace ist.extra) } in val_interp ist alias.Tacenv.alias_body >>= fun v -> - Ftactic.lift (catch_error_loc loc false (tactic_of_value ist v)) + Ftactic.lift (tactic_of_value ist v) in let tac = Ftactic.with_env interp_vars >>= fun (env, lr) -> @@ -1243,11 +1255,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false - (catch_error_tac_loc loc false trace (val_interp ~appl ist (Tacenv.interp_ltac r))) + (catch_error_tac_loc (* interp *) loc false trace + (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r))) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with - | TacGeneric arg -> interp_genarg ist arg + | TacGeneric (_,arg) -> interp_genarg ist arg | Reference r -> interp_ltac_reference false ist r | ConstrMayEval c -> Ftactic.enter begin fun gl -> @@ -1297,8 +1310,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = is not a tactic that expects arguments. Otherwise Ltac goes into an infinite loop (val_interp puts a VFun back on body, and then interp_app is called again...) *) - | (VFun(appl,trace,olfun,(_::_ as var),body) - |VFun(appl,trace,olfun,([] as var), + | (VFun(appl,trace,_,olfun,(_::_ as var),body) + |VFun(appl,trace,_,olfun,([] as var), (TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) -> let (extfun,lvar,lval)=head_with_value (var,largs) in let fold accu (id, v) = Id.Map.add id v accu in @@ -1312,7 +1325,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac_loc loc false trace (val_interp ist body)) >>= fun v -> + (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1333,8 +1346,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval else - Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body))) - | (VFun(appl,trace,olfun,[],body)) -> + Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body))) + | (VFun(appl,trace,_,olfun,[],body)) -> let extra_args = List.length largs in let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info @@ -1353,15 +1366,15 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = and tactic_of_value ist vle = if has_type vle (topwit wit_tacvalue) then match to_tacvalue vle with - | VFun (appl,trace,lfun,[],t) -> + | VFun (appl,trace,loc,lfun,[],t) -> Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) -> let ist = { lfun = lfun; poly; extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic_ist ist t) in - Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | VFun (appl,_,vmap,vars,_) -> + Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac_loc loc false trace tac) + | VFun (appl,_,loc,vmap,vars,_) -> let tactic_nm = match appl with UnnamedAppl -> "An unnamed user-defined tactic" @@ -1440,14 +1453,14 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = let ist = { ist with lfun } in val_interp ist lhs >>= fun v -> if has_type v (topwit wit_tacvalue) then match to_tacvalue v with - | VFun (appl,trace,lfun,[],t) -> + | VFun (appl,trace,loc,lfun,[],t) -> let ist = { lfun = lfun ; poly ; extra = TacStore.set ist.extra f_trace trace } in let tac = eval_tactic_ist ist t in - let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in + let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [], TacId []) in catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy)) | _ -> Ftactic.return v else Ftactic.return v @@ -1940,7 +1953,7 @@ module Value = struct include Taccoerce.Value let of_closure ist tac = - let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in + let closure = VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) in of_tacvalue closure let apply_expr f args = @@ -2028,6 +2041,9 @@ let () = declare_uniform wit_int let () = + declare_uniform wit_nat + +let () = declare_uniform wit_bool let () = diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index c2f1589b74..fd869b225f 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -237,7 +237,7 @@ and subst_tacarg subst = function | TacPretype c -> TacPretype (subst_glob_constr subst c) | TacNumgoals -> TacNumgoals | Tacexp t -> Tacexp (subst_tactic subst t) - | TacGeneric arg -> TacGeneric (subst_genarg subst arg) + | TacGeneric (isquot,arg) -> TacGeneric (isquot,subst_genarg subst arg) (* Reads the rules of a Match Context or a Match *) and subst_match_rule subst = function diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml index 148c1772bf..9008691bca 100644 --- a/plugins/micromega/certificate.ml +++ b/plugins/micromega/certificate.ml @@ -354,7 +354,7 @@ let is_linear_for v pc = *) let is_linear_substitution sys ((p, o), prf) = - let pred v = v =/ Q.one || v =/ Q.neg_one in + let pred v = v =/ Q.one || v =/ Q.minus_one in match o with | Eq -> ( match @@ -761,7 +761,7 @@ let reduce_unary psys = let is_unary_equation (cstr, prf) = if cstr.op == Eq then Vect.find - (fun v n -> if n =/ Q.one || n =/ Q.neg_one then Some v else None) + (fun v n -> if n =/ Q.one || n =/ Q.minus_one then Some v else None) cstr.coeffs else None in diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 44bc20e55f..d2c49c4432 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2141,6 +2141,7 @@ let really_call_csdpcert : List.fold_left Filename.concat (Envars.coqlib ()) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in + let cmdname = if Sys.file_exists cmdname then cmdname else "csdpcert" in match (command cmdname [|cmdname|] (provername, poly) : csdp_certificate) with | F str -> if debug then Printf.fprintf stdout "really_call_csdpcert : %s\n" str; diff --git a/plugins/micromega/dune b/plugins/micromega/dune index 33ad3a0138..204125ab56 100644 --- a/plugins/micromega/dune +++ b/plugins/micromega/dune @@ -4,7 +4,7 @@ ; be careful not to link the executable to the plugin! (modules (:standard \ csdpcert g_zify zify)) (synopsis "Coq's micromega plugin") - (libraries num coq.plugins.ltac)) + (libraries coq.plugins.ltac)) (executable (name csdpcert) diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml index 3d1770a541..f4d17b8940 100644 --- a/plugins/micromega/mfourier.ml +++ b/plugins/micromega/mfourier.ml @@ -190,6 +190,7 @@ let system_list sys = let add (v1, c1) (v2, c2) = assert (c1 <>/ Q.zero && c2 <>/ Q.zero); + (* XXX Can use Q.inv now *) let res = mul_add (Q.one // c1) v1 (Q.one // c2) v2 in (res, count res) @@ -569,7 +570,7 @@ module Fourier = struct (* We add a dummy (fresh) variable for vector *) let fresh = List.fold_left (fun fr c -> max fr (Vect.fresh c.coeffs)) 0 l in let cstr = - {coeffs = Vect.set fresh Q.neg_one vect; op = Eq; cst = Q.zero} + {coeffs = Vect.set fresh Q.minus_one vect; op = Eq; cst = Q.zero} in match solve fresh choose_equality_var choose_variable (cstr :: l) with | Inr prf -> None (* This is an unsatisfiability proof *) diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml index 4cb91ea520..02c4bab497 100644 --- a/plugins/micromega/numCompat.ml +++ b/plugins/micromega/numCompat.ml @@ -31,37 +31,24 @@ module type ZArith = sig end module Z = struct - type t = Big_int.big_int - - open Big_int - - let zero = zero_big_int - let one = unit_big_int - let two = big_int_of_int 2 - let add = Big_int.add_big_int - let sub = Big_int.sub_big_int - let mul = Big_int.mult_big_int - let div = Big_int.div_big_int - let neg = Big_int.minus_big_int - let sign = Big_int.sign_big_int - let equal = eq_big_int - let compare = compare_big_int - let power_int = power_big_int_positive_int - let quomod = quomod_big_int + (* Beware this only works fine in ZArith >= 1.10 due to + https://github.com/ocaml/Zarith/issues/58 *) + include Z - let ppcm x y = - let g = gcd_big_int x y in - let x' = div_big_int x g in - let y' = div_big_int y g in - mult_big_int g (mult_big_int x' y') - - let gcd = gcd_big_int + (* Constants *) + let two = Z.of_int 2 + let ten = Z.of_int 10 + let power_int = Big_int_Z.power_big_int_positive_int + let quomod = Big_int_Z.quomod_big_int - let lcm x y = - if eq_big_int x zero && eq_big_int y zero then zero - else abs_big_int (div_big_int (mult_big_int x y) (gcd x y)) + (* zarith fails with division by zero if x == 0 && y == 0 *) + let lcm x y = if Z.equal x zero && Z.equal y zero then zero else Z.lcm x y - let to_string = string_of_big_int + let ppcm x y = + let g = gcd x y in + let x' = Z.div x g in + let y' = Z.div y g in + Z.mul g (Z.mul x' y') end module type QArith = sig @@ -74,7 +61,7 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + val minus_one : t module Notations : sig val ( // ) : t -> t -> t @@ -119,56 +106,64 @@ end module Q : QArith with module Z = Z = struct module Z = Z - type t = Num.num + let pow_check_exp x y = + let z_res = + if y = 0 then Z.one + else if y > 0 then Z.pow x y + else (* s < 0 *) + Z.pow x (abs y) + in + let z_res = Q.of_bigint z_res in + if 0 <= y then z_res else Q.inv z_res - open Num + include Q - let of_int x = Int x - let zero = Int 0 - let one = Int 1 - let two = Int 2 - let ten = Int 10 - let neg_one = Int (-1) + let two = Q.(of_int 2) + let ten = Q.(of_int 10) module Notations = struct - let ( // ) = div_num - let ( +/ ) = add_num - let ( -/ ) = sub_num - let ( */ ) = mult_num - let ( =/ ) = eq_num - let ( <>/ ) = ( <>/ ) - let ( >/ ) = ( >/ ) - let ( >=/ ) = ( >=/ ) - let ( </ ) = ( </ ) - let ( <=/ ) = ( <=/ ) + let ( // ) = Q.div + let ( +/ ) = Q.add + let ( -/ ) = Q.sub + let ( */ ) = Q.mul + let ( =/ ) = Q.equal + let ( <>/ ) x y = not (Q.equal x y) + let ( >/ ) = Q.gt + let ( >=/ ) = Q.geq + let ( </ ) = Q.lt + let ( <=/ ) = Q.leq end - let compare = compare_num - let make x y = Big_int x // Big_int y - - let numdom r = - let r' = Ratio.normalize_ratio (ratio_of_num r) in - (Ratio.numerator_ratio r', Ratio.denominator_ratio r') - - let num x = numdom x |> fst - let den x = numdom x |> snd - let of_bigint x = Big_int x - let to_bigint = big_int_of_num - let neg = minus_num - - (* let inv = *) - let max = max_num - let min = min_num - let sign = sign_num - let abs = abs_num - let mod_ = mod_num - let floor = floor_num - let ceiling = ceiling_num - let round = round_num - let pow2 n = power_num two (Int n) - let pow10 n = power_num ten (Int n) - let power x = power_num (Int x) - let to_string = string_of_num - let of_string = num_of_string - let to_float = float_of_num + (* XXX: review / improve *) + let floorZ q : Z.t = Z.fdiv (num q) (den q) + let floor q : t = floorZ q |> Q.of_bigint + let ceiling q : t = Z.cdiv (Q.num q) (Q.den q) |> Q.of_bigint + let half = Q.make Z.one Z.two + + (* We imitate Num's round which is to the nearest *) + let round q = floor (Q.add half q) + + (* XXX: review / improve *) + let quo x y = + let s = sign y in + let res = floor (x / abs y) in + if Int.equal s (-1) then neg res else res + + let mod_ x y = x - (y * quo x y) + + (* XXX: review / improve *) + (* Note that Z.pow doesn't support negative exponents *) + + let pow2 y = pow_check_exp Z.two y + let pow10 y = pow_check_exp Z.ten y + + let power (x : int) (y : t) : t = + let y = + try Q.to_int y + with Z.Overflow -> + (* XXX: make doesn't link Pp / CErrors for csdpcert, that could be fixed *) + raise (Invalid_argument "[micromega] overflow in exponentiation") + (* CErrors.user_err (Pp.str "[micromega] overflow in exponentiation") *) + in + pow_check_exp (Z.of_int x) y end diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli index acc6be6ce0..0b4d52708f 100644 --- a/plugins/micromega/numCompat.mli +++ b/plugins/micromega/numCompat.mli @@ -25,8 +25,15 @@ module type ZArith = sig val power_int : t -> int -> t val quomod : t -> t -> t * t val ppcm : t -> t -> t + + (** [gcd x y] Greatest Common Divisor. Must always return a + positive number *) val gcd : t -> t -> t + + (** [lcm x y] Least Common Multiplier. Must always return a + positive number *) val lcm : t -> t -> t + val to_string : t -> string end @@ -40,7 +47,9 @@ module type QArith = sig val one : t val two : t val ten : t - val neg_one : t + + (** -1 constant *) + val minus_one : t module Notations : sig val ( // ) : t -> t -> t diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml index afef41d67e..5c0aa9ef0d 100644 --- a/plugins/micromega/polynomial.ml +++ b/plugins/micromega/polynomial.ml @@ -156,7 +156,7 @@ let pp_mon o (m, i) = if Monomial.is_const m then if Q.zero =/ i then () else Printf.fprintf o "%s" (Q.to_string i) else if Q.one =/ i then Monomial.pp o m - else if Q.neg_one =/ i then Printf.fprintf o "-%a" Monomial.pp m + else if Q.minus_one =/ i then Printf.fprintf o "-%a" Monomial.pp m else if Q.zero =/ i then () else Printf.fprintf o "%s*%a" (Q.to_string i) Monomial.pp m @@ -912,7 +912,7 @@ module WithProof = struct else match o with | Eq -> - Some ((Vect.set 0 Q.neg_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) + Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.Gcd (g, prf)) | Gt -> failwith "cutting_plane ignore strict constraints" | Ge -> (* This is a non-trivial common divisor *) @@ -999,7 +999,7 @@ module WithProof = struct | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p) let is_substitution strict ((p, o), prf) = - let pred v = if strict then v =/ Q.one || v =/ Q.neg_one else true in + let pred v = if strict then v =/ Q.one || v =/ Q.minus_one else true in match o with Eq -> LinPoly.search_linear pred p | _ -> None let subst1 sys0 = diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml index eaa26ded62..f59d65085a 100644 --- a/plugins/micromega/simplex.ml +++ b/plugins/micromega/simplex.ml @@ -247,8 +247,8 @@ let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t = let a = Vect.get c e in if a =/ Q.zero then failwith "Cannot solve column" else - let a' = Q.neg_one // a in - Vect.mul a' (Vect.set r Q.neg_one (Vect.set c Q.zero e)) + let a' = Q.minus_one // a in + Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e)) (** [pivot_row r c e] @param c is such that c = e @@ -364,7 +364,8 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t) if n >=/ Q.zero then Sat (t', None) else let v' = safe_find "push_real" nw t' in - Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.neg_one v'))) ) + Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v'))) + ) (** One complication is that equalities needs some pre-processing. *) @@ -399,7 +400,7 @@ let eliminate_equalities (vr0 : var) (l : Polynomial.cstr list) = elim (idx + 1) (vr + 1) (IMap.add vr (idx, true) vm) l ((vr, v) :: acc) | Eq -> let v1 = Vect.set 0 (Q.neg c.cst) c.coeffs in - let v2 = Vect.mul Q.neg_one v1 in + let v2 = Vect.mul Q.minus_one v1 in let vm = IMap.add vr (idx, true) (IMap.add (vr + 1) (idx, false) vm) in elim (idx + 1) (vr + 2) vm l ((vr, v1) :: (vr + 1, v2) :: acc) | Gt -> raise Strict ) diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index 2b04bb80e2..aeb9d14555 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -80,7 +80,7 @@ let is_zero (d, v) = match v with Empty -> true | _ -> false (* Vectors. Conventionally indexed 1..n. *) (* ------------------------------------------------------------------------- *) -let vector_0 n = ((n, undefined) : vector) +let vector_0 n : vector = (n, undefined) let dim (v : vector) = fst v let vector_const c n = @@ -99,7 +99,7 @@ let vector_of_list l = (* Matrices; again rows and columns indexed from 1. *) (* ------------------------------------------------------------------------- *) -let matrix_0 (m, n) = (((m, n), undefined) : matrix) +let matrix_0 (m, n) : matrix = ((m, n), undefined) let dimensions (m : matrix) = fst m let matrix_cmul c (m : matrix) = @@ -107,7 +107,7 @@ let matrix_cmul c (m : matrix) = if c =/ Q.zero then matrix_0 (i, j) else ((i, j), mapf (fun x -> c */ x) (snd m)) -let matrix_neg (m : matrix) = ((dimensions m, mapf Q.neg (snd m)) : matrix) +let matrix_neg (m : matrix) : matrix = (dimensions m, mapf Q.neg (snd m)) let matrix_add (m1 : matrix) (m2 : matrix) = let d1 = dimensions m1 and d2 = dimensions m2 in @@ -138,7 +138,7 @@ let diagonal (v : vector) = (* Monomials. *) (* ------------------------------------------------------------------------- *) let monomial_1 = (undefined : monomial) -let monomial_var x = (x |=> 1 : monomial) +let monomial_var x : monomial = x |=> 1 let (monomial_mul : monomial -> monomial -> monomial) = combine ( + ) (fun x -> false) @@ -152,16 +152,16 @@ let monomial_variables m = dom m (* ------------------------------------------------------------------------- *) let poly_0 = (undefined : poly) let poly_isconst (p : poly) = foldl (fun a m c -> m = monomial_1 && a) true p -let poly_var x = (monomial_var x |=> Q.one : poly) +let poly_var x : poly = monomial_var x |=> Q.one let poly_const c = if c =/ Q.zero then poly_0 else monomial_1 |=> c let poly_cmul c (p : poly) = if c =/ Q.zero then poly_0 else mapf (fun x -> c */ x) p -let poly_neg (p : poly) = (mapf Q.neg p : poly) +let poly_neg (p : poly) : poly = mapf Q.neg p -let poly_add (p1 : poly) (p2 : poly) = - (combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 : poly) +let poly_add (p1 : poly) (p2 : poly) : poly = + combine ( +/ ) (fun x -> x =/ Q.zero) p1 p2 let poly_sub p1 p2 = poly_add p1 (poly_neg p2) @@ -576,7 +576,7 @@ let eliminate_all_equations one = else let v = choose_variable eq in let a = apply eq v in - let eq' = equation_cmul (Q.neg_one // a) (undefine v eq) in + let eq' = equation_cmul (Q.minus_one // a) (undefine v eq) in let elim e = let b = tryapplyd e v Q.zero in if b =/ Q.zero then e @@ -814,7 +814,7 @@ let bmatrix_add = combine ( +/ ) (fun x -> x =/ Q.zero) let bmatrix_cmul c bm = if c =/ Q.zero then undefined else mapf (fun x -> c */ x) bm -let bmatrix_neg = bmatrix_cmul Q.neg_one +let bmatrix_neg = bmatrix_cmul Q.minus_one (* ------------------------------------------------------------------------- *) (* Smash a block matrix into components. *) @@ -943,7 +943,7 @@ let real_positivnullstellensatz_general linf d eqs leqs pol = List.fold_right (fun k -> List.nth pvs (k - 1) |-> element vec k) (1 -- dim vec) - ((0, 0, 0) |=> Q.neg_one) + ((0, 0, 0) |=> Q.minus_one) in let finalassigs = foldl (fun a v e -> (v |-> equation_eval newassigs e) a) newassigs allassig @@ -1166,7 +1166,7 @@ let sumofsquares_general_symmetry tool pol = match cls with | [] -> raise Sanity | [h] -> acc - | h :: t -> List.map (fun k -> (k |-> Q.neg_one) (h |=> Q.one)) t @ acc + | h :: t -> List.map (fun k -> (k |-> Q.minus_one) (h |=> Q.one)) t @ acc in List.fold_right mk_eq eqvcls [] in @@ -1191,14 +1191,13 @@ let sumofsquares_general_symmetry tool pol = let diagents = end_itlist equation_add (List.map (fun i -> apply allassig (i, i)) (1 -- n)) in - let mk_matrix v = - ( ( (n, n) - , foldl - (fun m (i, j) ass -> - let c = tryapplyd ass v Q.zero in - if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) - undefined allassig ) - : matrix ) + let mk_matrix v : matrix = + ( (n, n) + , foldl + (fun m (i, j) ass -> + let c = tryapplyd ass v Q.zero in + if c =/ Q.zero then m else ((j, i) |-> c) (((i, j) |-> c) m)) + undefined allassig ) in let mats = List.map mk_matrix qvars and obj = diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml index 3e0b1f2cd9..4df32f2ba4 100644 --- a/plugins/micromega/vect.ml +++ b/plugins/micromega/vect.ml @@ -52,7 +52,7 @@ let pp_var_num pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "-%a" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "-%a" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v @@ -60,7 +60,7 @@ let pp_var_num_smt pp_var o {var = v; coe = n} = if Int.equal v 0 then if Q.zero =/ n then () else Printf.fprintf o "%s" (Q.to_string n) else if Q.one =/ n then pp_var o v - else if Q.neg_one =/ n then Printf.fprintf o "(- %a)" pp_var v + else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v else if Q.zero =/ n then () else Printf.fprintf o "(* %s %a)" (Q.to_string n) pp_var v diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 6ed6b8da91..5f5a974b6a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -127,8 +127,8 @@ let closed_term_ast = let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(CAst.make (tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); - TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) + [TacGeneric (None, Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); + TacGeneric (None, Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -200,7 +200,7 @@ let exec_tactic env evd n f args = (* Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (CAst.make (get_res, [TacGeneric n])) in + let get_res = TacML (CAst.make (get_res, [TacGeneric (None, n)])) in let getter = Tacexp (TacFun (List.map (fun n -> Name n) lid, get_res)) in (* Evaluate the whole result *) let gl = dummy_goal env evd in diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 60af804c1b..b32b58062a 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -219,20 +219,20 @@ let test_ssrslashnum b1 b2 _ strm = match Util.stream_nth 0 strm with | Tok.KEYWORD "/" -> (match Util.stream_nth 1 strm with - | Tok.NUMERAL _ when b1 -> + | Tok.NUMBER _ when b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> () | Tok.KEYWORD "/" -> if not b2 then () else begin match Util.stream_nth 3 strm with - | Tok.NUMERAL _ -> () + | Tok.NUMBER _ -> () | _ -> raise Stream.Failure end | _ -> raise Stream.Failure) | Tok.KEYWORD "/" when not b1 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 3 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -243,7 +243,7 @@ let test_ssrslashnum b1 b2 _ strm = | Tok.KEYWORD "//" when not b1 -> (match Util.stream_nth 1 strm with | Tok.KEYWORD "=" when not b2 -> () - | Tok.NUMERAL _ when b2 -> + | Tok.NUMBER _ when b2 -> (match Util.stream_nth 2 strm with | Tok.KEYWORD "=" -> () | _ -> raise Stream.Failure) @@ -1682,7 +1682,7 @@ let set_pr_ssrtac name prec afmt = (* FIXME *) () (* let ssrtac_expr ?loc name args = TacML (CAst.make ?loc (ssrtac_entry name, args)) let tclintros_expr ?loc tac ipats = - let args = [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in + let args = [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrintrosarg) (tac, ipats))] in ssrtac_expr ?loc "tclintros" args } @@ -1777,7 +1777,7 @@ let _ = set_pr_ssrtac "tcldo" 3 [ArgSep "do "; ArgSsr "doarg"] let ssrdotac_expr ?loc n m tac clauses = let arg = ((n, m), tac), clauses in - ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (in_gen (rawwit wit_ssrdoarg) arg)] + ssrtac_expr ?loc "tcldo" [Tacexpr.TacGeneric (None, in_gen (rawwit wit_ssrdoarg) arg)] } @@ -1828,7 +1828,7 @@ let tclseq_expr ?loc tac dir arg = let arg1 = in_gen (rawwit wit_ssrtclarg) tac in let arg2 = in_gen (rawwit wit_ssrseqdir) dir in let arg3 = in_gen (rawwit wit_ssrseqarg) (check_seqtacarg dir arg) in - ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric x) [arg1; arg2; arg3]) + ssrtac_expr ?loc "tclseq" (List.map (fun x -> Tacexpr.TacGeneric (None, x)) [arg1; arg2; arg3]) } @@ -2451,7 +2451,7 @@ GRAMMAR EXTEND Gram tactic_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> { ssrtac_expr ~loc "abstract" - [Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; + [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; END TACTIC EXTEND ssrabstract | [ "abstract" ssrdgens(gens) ] -> { diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg index e66dbe17b2..c030925ea9 100644 --- a/plugins/syntax/g_numeral.mlg +++ b/plugins/syntax/g_numeral.mlg @@ -24,6 +24,11 @@ let pr_numnot_option = function | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")" | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")" +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + } VERNAC ARGUMENT EXTEND numnotoption @@ -34,8 +39,13 @@ VERNAC ARGUMENT EXTEND numnotoption END VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":" ident(sc) numnotoption(o) ] -> { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) numnotoption(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o } END |