diff options
Diffstat (limited to 'plugins')
60 files changed, 1040 insertions, 948 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 23f8fe04a3..ac2058ba1b 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -115,7 +115,7 @@ module Bool = struct | Case (info, r, _iv, arg, pats) -> let is_bool = let i = info.ci_ind in - Names.eq_ind i (Lazy.force ind) + Names.Ind.CanOrd.equal i (Lazy.force ind) in if is_bool then Ifb ((aux arg), (aux pats.(0)), (aux pats.(1))) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 6f5c910297..129b220680 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -145,7 +145,7 @@ let rec term_equal t1 t2 = | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2 | Constructor {ci_constr=(c1,u1); ci_arity=i1; ci_nhyps=j1}, Constructor {ci_constr=(c2,u2); ci_arity=i2; ci_nhyps=j2} -> - Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2 (* FIXME check eq? *) + Int.equal i1 i2 && Int.equal j1 j2 && Construct.CanOrd.equal c1 c2 (* FIXME check eq? *) | _ -> false open Hashset.Combine @@ -155,7 +155,7 @@ let rec hash_term = function | Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2) | Eps i -> combine 3 (Id.hash i) | Appli (t1, t2) -> combine3 4 (hash_term t1) (hash_term t2) - | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (constructor_hash c) i j + | Constructor {ci_constr=(c,u); ci_arity=i; ci_nhyps=j} -> combine4 5 (Construct.CanOrd.hash c) i j type ccpattern = PApp of term * ccpattern list (* arguments are reversed *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 2dca1d5e49..6869f9c47e 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args = (* Can we instantiate types variables for this constant ? *) (* In Ocaml, inside the definition of this constant, the answer is no. *) let instantiated = - if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints + if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints then var2var' (snd schema) else instantiation schema in diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index b1ce10985a..21ec80abbc 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -685,7 +685,7 @@ let is_regular_match br = | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> Ind.CanOrd.equal ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f8449bcda1..e56d66ca2d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -32,7 +32,7 @@ module Refset' = GlobRef.Set_env let occur_kn_in_ref kn = let open GlobRef in function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' + | ConstructRef ((kn',_),_) -> MutInd.CanOrd.equal kn kn' | ConstRef _ | VarRef _ -> false let repr_of_r = let open GlobRef in function diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 6ddc6ba21e..d6790d008a 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -108,10 +108,6 @@ let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (Pputils.pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global -let warn_deprecated_syntax = - CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated" - (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator") - } ARGUMENT EXTEND firstorder_using @@ -119,12 +115,7 @@ ARGUMENT EXTEND firstorder_using PRINTED BY { pr_firstorder_using_typed } RAW_PRINTED BY { pr_firstorder_using_raw } GLOB_PRINTED BY { pr_firstorder_using_glob } -| [ "using" reference(a) ] -> { [a] } -| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> { a::l } -| [ "using" reference(a) reference(b) reference_list(l) ] -> { - warn_deprecated_syntax (); - a::b::l - } +| [ "using" ne_reference_list_sep(l,",") ] -> { l } | [ ] -> { [] } END diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index f13901c36d..4adad53899 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -38,7 +38,7 @@ let compare_gr id1 id2 = if id1==id2 then 0 else if id1==dummy_id then 1 else if id2==dummy_id then -1 - else GlobRef.Ordered.compare id1 id2 + else GlobRef.CanOrd.compare id1 id2 module OrderedInstance= struct diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index db3631daa4..99c5f85125 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -62,7 +62,7 @@ module Hitem= struct type t = h_item let compare (id1,co1) (id2,co2)= - let c = GlobRef.Ordered.compare id1 id2 in + let c = GlobRef.CanOrd.compare id1 id2 in if c = 0 then let cmp (i1, c1) (i2, c2) = let c = Int.compare i1 i2 in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index e50c6087bb..73eb943418 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -674,7 +674,7 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos |Prod _ -> let new_infos = {dyn_infos with info = (f, args)} in build_proof_args env sigma do_finalize new_infos - | Const (c, _) when not (List.mem_f Constant.equal c fnames) -> + | Const (c, _) when not (List.mem_f Constant.CanOrd.equal c fnames) -> let new_infos = {dyn_infos with info = (f, args)} in (* Pp.msgnl (str "proving in " ++ pr_lconstr_env (pf_env g) dyn_infos.info); *) build_proof_args env sigma do_finalize new_infos diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 1ab747ca09..0ab9ac65d7 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -100,8 +100,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in let is_dom c = match Constr.kind c with - | Ind ((u, _), _) -> MutInd.equal u rel_as_kn - | Construct (((u, _), _), _) -> MutInd.equal u rel_as_kn + | Ind ((u, _), _) -> Environ.QMutInd.equal env u rel_as_kn + | Construct (((u, _), _), _) -> Environ.QMutInd.equal env u rel_as_kn | _ -> false in let get_fun_num c = diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index bbc4df7dde..ca6ae150a7 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -147,19 +147,19 @@ END module Vernac = Pvernac.Vernac_ module Tactic = Pltac -let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = - Genarg.create_arg "function_rec_definition_loc" +let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) = + Genarg.create_arg "function_fix_definition" -let function_rec_definition_loc = - Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc) +let function_fix_definition = + Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition) } GRAMMAR EXTEND Gram - GLOBAL: function_rec_definition_loc ; + GLOBAL: function_fix_definition ; - function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]] + function_fix_definition: + [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]] ; END @@ -168,7 +168,7 @@ END let () = let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in - Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer + Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer let is_proof_termination_interactively_checked recsl = List.exists (function @@ -196,7 +196,7 @@ let is_interactive recsl = } VERNAC COMMAND EXTEND Function STATE CUSTOM -| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] +| ["Function" ne_function_fix_definition_list_sep(recsl,"with")] => { classify_funind recsl } -> { if is_interactive recsl then diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 012fcee486..314c8abcaf 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1316,9 +1316,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in List.map - (function - | cst -> List.assoc_f Constant.equal (fst cst) this_block_funs_indexes) + (function cst -> List.assoc_f eq (fst cst) this_block_funs_indexes) funs in let ind_list = @@ -2228,7 +2228,8 @@ let build_case_scheme fa = let prop_sort = Sorts.InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc_f Constant.equal funs this_block_funs_indexes + let eq c1 c2 = Environ.QConstant.equal env c1 c2 in + List.assoc_f eq funs this_block_funs_indexes in let ind, sf = let ind = (first_fun_kn, funs_indexes) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6ed61043f9..767a9ec39b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env = let constructors = Inductiveops.get_constructors env indf in let constructor : Inductiveops.constructor_summary = List.find - (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr)) + (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr)) (Array.to_list constructors) in let cs_args_types : types list = @@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ = let constructors = Inductiveops.get_constructors env indf in let constructor = List.find - (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr) + (fun cs -> + Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr) (Array.to_list constructors) in let cs_args_types : types list = diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 8e1331ace9..164a446fe3 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -444,7 +444,8 @@ let rec are_unifiable_aux = function match (DAst.get l, DAst.get r) with | PatVar _, _ | _, PatVar _ -> are_unifiable_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs @@ -464,7 +465,8 @@ let rec eq_cases_pattern_aux = function match (DAst.get l, DAst.get r) with | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs | PatCstr (constructor1, cpl1, _), PatCstr (constructor2, cpl2, _) -> - if not (eq_constructor constructor2 constructor1) then raise NotUnifiable + if not (Construct.CanOrd.equal constructor2 constructor1) then + raise NotUnifiable else let eqs' = try List.combine cpl1 cpl2 @ eqs diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 0179215d6a..6464556e4e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -108,7 +108,7 @@ let with_full_print f a = Constrextern.print_universes := old_printuniverses; Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; - Dumpglob.continue (); + Dumpglob.pop_output (); res with reraise -> Impargs.make_implicit_args old_implicit_args; @@ -118,7 +118,7 @@ let with_full_print f a = Constrextern.print_universes := old_printuniverses; Goptions.set_bool_option_value Detyping.print_allow_match_default_opt_name old_printallowmatchdefaultclause; - Dumpglob.continue (); + Dumpglob.pop_output (); raise reraise (**********************) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5d631aac84..118a917381 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -27,12 +27,13 @@ open Indfun_common *) let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl -> + let env = Proofview.Goal.env gl in let sigma = project gl in let typ = pf_get_hyp_typ hid gl in match EConstr.kind sigma typ with | App (i, args) when isInd sigma i -> let ((kn', num) as ind'), u = destInd sigma i in - if MutInd.equal kn kn' then + if Environ.QMutInd.equal env kn kn' then (* We have generated a graph hypothesis so that we must change it if we can *) let info = match find_Function_of_graph ind' with diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg index ad4374dba3..ff4a82f864 100644 --- a/plugins/ltac/extraargs.mlg +++ b/plugins/ltac/extraargs.mlg @@ -41,7 +41,7 @@ let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_simpl let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in - Tacentries.create_ltac_quotation "ltac" inject (Pltac.tactic_expr, Some 5) + Tacentries.create_ltac_quotation "ltac" inject (Pltac.ltac_expr, Some 5) (** Backward-compatible tactic notation entry names *) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 44472a1995..7e8400910c 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -116,12 +116,25 @@ END let make_depth n = snd (Eauto.make_dimension n None) +(* deprecated in 8.13; the second int_or_var will be removed *) +let deprecated_eauto_bfs = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [eauto @int_or_var @int_or_var] is deprecated. Use [bfs eauto] instead.") + +let deprecated_bfs tacname = + CWarnings.create + ~name:"eauto_bfs" ~category:"deprecated" + (fun () -> Pp.str "The syntax [" ++ Pp.str tacname ++ Pp.str "@int_or_var @int_or_var] is deprecated. No replacement yet.") + } TACTIC EXTEND eauto | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> deprecated_eauto_bfs () | _ -> () ); + Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND new_eauto @@ -135,13 +148,17 @@ END TACTIC EXTEND debug_eauto | [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "debug eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND info_eauto | [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) hintbases(db) ] -> - { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } + { + ( match n,p with Some _, Some _ -> (deprecated_bfs "info_eauto") () | _ -> () ); + Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } END TACTIC EXTEND dfs_eauto @@ -150,6 +167,12 @@ TACTIC EXTEND dfs_eauto { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } END +TACTIC EXTEND bfs_eauto +| [ "bfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (true, Eauto.make_depth p) (eval_uconstrs ist lems) db } +END + TACTIC EXTEND autounfold | [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } END @@ -240,10 +263,21 @@ ARGUMENT EXTEND opthints END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF -| #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in - Hints.add_hints ~locality - (match dbnames with None -> ["core"] | Some l -> l) entry; +| #[ locality = Attributes.option_locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { + let open Goptions in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + let () = match locality with + | OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); + | OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); + | OptDefault | OptLocal -> () + in + Hints.add_hints ~locality + (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 6cf5d30a95..c2e95c45f9 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -74,22 +74,22 @@ let hint = G_proofs.hint } GRAMMAR EXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + GLOBAL: tactic tacdef_body ltac_expr binder_tactic tactic_value command hint tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; + term; tactic_then_last: - [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + [ [ "|"; lta = LIST0 (OPT ltac_expr) SEP "|" -> { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } | -> { [||] } ] ] ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } - | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + for_each_goal: + [ [ ta = ltac_expr; "|"; tg = for_each_goal -> { let (first,last) = tg in (ta::first, last) } + | ta = ltac_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } - | ta = tactic_expr -> { ([ta], None) } - | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | ta = ltac_expr -> { ([ta], None) } + | "|"; tg = for_each_goal -> { let (first,last) = tg in (TacId [] :: first, last) } | -> { ([TacId []], None) } ] ] ; @@ -97,13 +97,13 @@ GRAMMAR EXTEND Gram for [TacExtend] *) [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] ; - tactic_expr: + ltac_expr: [ "5" RIGHTA [ te = binder_tactic -> { te } ] | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } - | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + [ ta0 = ltac_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = ltac_expr; ";"; ta1 = ltac_expr -> { TacThen (ta0,ta1) } + | ta0 = ltac_expr; ";"; l = tactic_then_locality; tg = for_each_goal; "]" -> { let (first,tail) = tg in match l , tail with | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) @@ -111,51 +111,51 @@ GRAMMAR EXTEND Gram | false , None -> TacThen (ta0,TacDispatch first) | true , None -> TacThens (ta0,first) } ] | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> { TacTry ta } - | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } - | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } - | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } - | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } - | IDENT "once"; ta = tactic_expr -> { TacOnce ta } - | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } - | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } + [ IDENT "try"; ta = ltac_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = ltac_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = ltac_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = ltac_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = ltac_expr -> { TacRepeat ta } + | IDENT "progress"; ta = ltac_expr -> { TacProgress ta } + | IDENT "once"; ta = ltac_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = ltac_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = ltac_expr -> { TacShowHyps ta } (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } | IDENT "abstract"; tc = NEXT; "using"; s = ident -> { TacAbstract (tc,Some s) } - | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] + | IDENT "only"; sel = selector; ":"; ta = ltac_expr -> { TacSelect (sel, ta) } ] (*End of To do*) | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + [ ta0 = ltac_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = ltac_expr; "+"; ta1 = ltac_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = ltac_expr ; + "then" ; tat = ltac_expr ; + "else" ; tae = ltac_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = ltac_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = ltac_expr; "||"; ta1 = ltac_expr -> { TacOrelse (ta0,ta1) } ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,false,mrl) } | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> { TacMatchGoal (b,true,mrl) } - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + | b = match_key; c = ltac_expr; "with"; mrl = match_list; "end" -> { TacMatch (b,c,mrl) } - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "first" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst l } - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + | IDENT "solve" ; "["; l = LIST0 ltac_expr SEP "|"; "]" -> { TacSolve l } | IDENT "idtac"; l = LIST0 message_token -> { TacId l } | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; l = LIST0 message_token -> { TacFail (g,n,l) } | st = simple_tactic -> { st } - | a = tactic_arg -> { TacArg(CAst.make ~loc a) } - | r = reference; la = LIST0 tactic_arg_compat -> + | a = tactic_value -> { TacArg(CAst.make ~loc a) } + | r = reference; la = LIST0 tactic_arg -> { TacArg(CAst.make ~loc @@ TacCall (CAst.make ~loc (r,la))) } ] | "0" - [ "("; a = tactic_expr; ")" -> { a } - | "["; ">"; tg = tactic_then_gen; "]" -> { + [ "("; a = ltac_expr; ")" -> { a } + | "["; ">"; tg = for_each_goal; "]" -> { let (tf,tail) = tg in begin match tail with | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) @@ -166,24 +166,24 @@ GRAMMAR EXTEND Gram failkw: [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] ; - (* binder_tactic: level 5 of tactic_expr *) + (* binder_tactic: level 5 of ltac_expr *) binder_tactic: [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + [ "fun"; it = LIST1 input_fun ; "=>"; body = ltac_expr LEVEL "5" -> { TacFun (it,body) } | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] + body = ltac_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } ] ] ; (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> { a } + tactic_arg: + [ [ a = tactic_value -> { 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 (None, genarg_of_unit ()) } ] ] ; (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: + tactic_value: [ [ c = constr_eval -> { ConstrMayEval c } | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } | IDENT "type_term"; c=uconstr -> { TacPretype c } @@ -223,20 +223,20 @@ GRAMMAR EXTEND Gram | l = ident -> { Name.Name l } ] ] ; let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } - | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = ltac_expr -> { (na, arg_of_expr te) } - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + | idr = identref; args = LIST1 input_fun; ":="; te = ltac_expr -> { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> + "["; pc = Constr.cpattern; "]" -> { Subterm (oid, pc) } - | pc = Constr.lconstr_pattern -> { Term pc } ] ] + | pc = Constr.cpattern -> { Term pc } ] ] ; - match_hyps: + match_hyp: [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } | na = name; ":="; mpv = match_pattern -> @@ -250,19 +250,19 @@ GRAMMAR EXTEND Gram ] ] ; match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyp SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = ltac_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_context_list: [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] ; match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } - | "_"; "=>"; te = tactic_expr -> { All te } ] ] + [ [ mp = match_pattern; "=>"; te = ltac_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = ltac_expr -> { All te } ] ] ; match_list: [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } @@ -282,13 +282,13 @@ GRAMMAR EXTEND Gram (* Definitions for tactics *) tacdef_body: [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> + redef = ltac_def_kind; body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) else let id = reference_to_id name in Tacexpr.TacticDefinition (id, TacFun (it, body)) } | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> + body = ltac_expr -> { if redef then Tacexpr.TacticRedefinition (name, body) else let id = reference_to_id name in @@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram ] ] ; tactic: - [ [ tac = tactic_expr -> { tac } ] ] + [ [ tac = ltac_expr -> { tac } ] ] ; range_selector: @@ -314,15 +314,12 @@ GRAMMAR EXTEND Gram { let open Goal_select in Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] ; - selector_body: + selector: [ [ l = range_selector_or_nth -> { l } | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] - ; toplevel_selector: - [ [ sel = selector_body; ":" -> { sel } + [ [ sel = selector; ":" -> { sel } | "!"; ":" -> { Goal_select.SelectAlreadyFocused } | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] ; @@ -332,19 +329,19 @@ GRAMMAR EXTEND Gram ; command: [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] -> + l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] -> { Vernacexpr.VernacProof (Some (in_tac ta), l) } - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] -> - { Vernacexpr.VernacProof (ta,Some l) } ] ] + | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr; + "with"; ta = Pltac.tactic -> + { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ] ; hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ] ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + term: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" -> { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] ; @@ -402,7 +399,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in ComTactic.solve g ~info t ~with_end_tac } END @@ -415,7 +412,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof VtProofStep{ proof_block_detection = pbr } } -> { let t, abstract = rm_abstract t in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END @@ -469,7 +466,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - { Feedback.msg_notice (Tacintern.print_ltac r) } + { Feedback.msg_notice (Tacentries.print_ltac r) } END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index ee94fd565a..a3f03b5bb5 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -67,12 +67,12 @@ END { type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (glob_constr_and_expr, Tacexpr.glob_red_expr) strategy_ast let interp_strategy ist gl s = let sigma = project gl in - sigma, strategy_of_ast s -let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s + sigma, strategy_of_ast ist s +let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (Tacintern.intern_red_expr ist) s let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" @@ -80,12 +80,9 @@ let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) = let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy (prc env sigma) prr s let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) = - let prr = Pptactic.pr_red_expr env sigma - (Ppconstr.pr_constr_expr, - Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_qualid, - Ppconstr.pr_constr_expr) - in + let prpat env sigma (_,c,_) = prc env sigma c in + let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in + let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prpat) in Rewrite.pr_strategy (prc env sigma) prr s } @@ -130,15 +127,15 @@ END { let db_strat db = StratUnary (Topdown, StratHints (false, db)) -let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) +let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast ist (db_strat db)) } TACTIC EXTEND rewrite_strat | [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) } | [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None } -| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) } -| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None } +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) } +| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None } END { diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index c186a83a5c..236de65462 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with end | _ -> ElimOnConstr clbind -let mkNumeral n = - Numeral (NumTok.Signed.of_int_string (string_of_int n)) +let mkNumber n = + Number (NumTok.Signed.of_int_string (string_of_int n)) let mkTacCase with_evar = function | [(clear,ElimOnConstr cl),(None,None),None],None -> @@ -130,7 +130,7 @@ let mkTacCase with_evar = function (* Reinterpret numbers as a notation for terms *) | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, - (clear,(CAst.make @@ CPrim (mkNumeral n), + (clear,(CAst.make @@ CPrim (mkNumber n), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) @@ -291,7 +291,7 @@ GRAMMAR EXTEND Gram ; simple_intropattern: [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + l = LIST0 ["%"; c = term LEVEL "0" -> { c } ] -> { let {CAst.loc=loc0;v=pat} = pat in let f c pat = let loc1 = Constrexpr_ops.constr_loc c in @@ -320,7 +320,7 @@ GRAMMAR EXTEND Gram with_bindings: [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] ; - red_flags: + red_flag: [ [ IDENT "beta" -> { [FBeta] } | IDENT "iota" -> { [FMatch;FFix;FCofix] } | IDENT "match" -> { [FMatch] } @@ -337,7 +337,7 @@ GRAMMAR EXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + [ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) } | d = delta_flag -> { all_with d } ] ] ; @@ -450,6 +450,11 @@ GRAMMAR EXTEND Gram ; as_or_and_ipat: [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat } + | "as"; ipat = equality_intropattern -> + { match ipat with + | IntroRewrite _ -> user_err Pp.(str "Disjunctive/conjunctive pattern expected.") + | IntroInjection _ -> user_err Pp.(strbrk "Found an injection pattern while a disjunctive/conjunctive pattern was expected; use " ++ str "\"injection as pattern\"" ++ strbrk " instead.") + | _ -> assert false } | -> { None } ] ] ; eqn_ipat: @@ -460,7 +465,7 @@ GRAMMAR EXTEND Gram [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] ; by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + [ [ "by"; tac = ltac_expr LEVEL "3" -> { Some tac } | -> { None } ] ] ; rewriter : diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index b7b54143df..94e398fe5d 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -37,8 +37,10 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Entry.create "tactic_arg" -let tactic_expr = Entry.create "tactic_expr" +let tactic_value = Entry.create "tactic_value" +let tactic_arg = tactic_value +let ltac_expr = Entry.create "ltac_expr" +let tactic_expr = ltac_expr let binder_tactic = Entry.create "binder_tactic" let tactic = Entry.create "tactic" diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 8565c4b4d6..3a4a081c93 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -31,8 +31,12 @@ val simple_tactic : raw_tactic_expr Entry.t val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t val in_clause : Names.lident Locus.clause_expr Entry.t val clause_dft_concl : Names.lident Locus.clause_expr Entry.t +val tactic_value : raw_tactic_arg Entry.t val tactic_arg : raw_tactic_arg Entry.t + [@@deprecated "Deprecated in 8.13; use 'tactic_value' instead"] +val ltac_expr : raw_tactic_expr Entry.t val tactic_expr : raw_tactic_expr Entry.t + [@@deprecated "Deprecated in 8.13; use 'ltac_expr' instead"] val binder_tactic : raw_tactic_expr Entry.t val tactic : raw_tactic_expr Entry.t val tactic_eoi : raw_tactic_expr Entry.t diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index fe896f9351..edd56ee0f7 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1135,8 +1135,8 @@ let pr_goal_selector ~toplevel s = pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env)); pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env)); pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env)); - pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env)); pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env)); + pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env)); pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = Pputils.pr_glb_generic; @@ -1334,8 +1334,8 @@ let () = ; Genprint.register_print0 wit_constr - (lift_env Ppconstr.pr_lconstr_expr) - (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c)) + (lift_env Ppconstr.pr_constr_expr) + (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 6a9fb5c2ea..5e199dad62 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -(** This module implements pretty-printers for tactic_expr syntactic +(** This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents. *) open Genarg diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index ff24e38577..8196ba6555 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -769,7 +769,7 @@ let get_rew_prf evars r = match r.rew_prf with let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation -let resolve_subrelation env avoid car rel sort prf rel' res = +let resolve_subrelation env car rel sort prf rel' res = if Termops.eq_constr (fst res.rew_evars) rel rel' then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in @@ -779,7 +779,7 @@ let resolve_subrelation env avoid car rel sort prf rel' res = rew_prf = RewPrf (rel', appsub); rew_evars = evars } -let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) evars = +let resolve_morphism env m args args' (b,cstr) evars = let evars, morph_instance, proj, sigargs, m', args, args' = let first = match (Array.findi (fun _ b -> not (Option.is_empty b)) args') with | Some i -> i @@ -843,18 +843,18 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev let proof = applist (proj, List.rev projargs) in let newt = applist (m', List.rev typeargs) in match respars with - [ a, Some r ] -> evars, proof, substl subst a, substl subst r, oldt, fnewt newt + [ a, Some r ] -> evars, proof, substl subst a, substl subst r, newt | _ -> assert(false) -let apply_constraint env avoid car rel prf cstr res = +let apply_constraint env car rel prf cstr res = match snd cstr with | None -> res - | Some r -> resolve_subrelation env avoid car rel (fst cstr) prf r res + | Some r -> resolve_subrelation env car rel (fst cstr) prf r res -let coerce env avoid cstr res = +let coerce env cstr res = let evars, (rel, prf) = get_rew_prf res.rew_evars res in let res = { res with rew_evars = evars } in - apply_constraint env avoid res.rew_car rel prf cstr res + apply_constraint env res.rew_car rel prf cstr res let apply_rule unify loccs : int pure_strategy = let (nowhere_except_in,occs) = convert_occs loccs in @@ -863,7 +863,7 @@ let apply_rule unify loccs : int pure_strategy = then List.mem occ occs else not (List.mem occ occs) in - { strategy = fun { state = occ ; env ; unfresh ; + { strategy = fun { state = occ ; env ; term1 = t ; ty1 = ty ; cstr ; evars } -> let unif = if isEvar (goalevars evars) t then None else unify env evars t in match unif with @@ -874,7 +874,7 @@ let apply_rule unify loccs : int pure_strategy = else if Termops.eq_constr (fst rew.rew_evars) t rew.rew_to then (occ, Identity) else let res = { rew with rew_car = ty } in - let res = Success (coerce env unfresh cstr res) in + let res = Success (coerce env cstr res) in (occ, res) } @@ -968,7 +968,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> + | App (f', args) when QConstant.equal env (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta env sigma (mkApp (v, args)) @@ -1017,10 +1017,10 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | None -> false | Some r -> not (is_rew_cast r.rew_prf)) args' then - let evars', prf, car, rel, c1, c2 = - resolve_morphism env unfresh t m args args' (prop, cstr') evars' + let evars', prf, car, rel, c2 = + resolve_morphism env m args args' (prop, cstr') evars' in - let res = { rew_car = ty; rew_from = c1; + let res = { rew_car = ty; rew_from = t; rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = evars' } in Success res @@ -1071,7 +1071,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = let res = match prf with | RewPrf (rel, prf) -> - Success (apply_constraint env unfresh res.rew_car + Success (apply_constraint env res.rew_car rel prf (prop,cstr) res) | _ -> Success res in state, res @@ -1094,20 +1094,6 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Fail | Identity -> res in state, res - (* if x' = None && flags.under_lambdas then *) - (* let lam = mkLambda (n, x, b) in *) - (* let lam', occ = aux env lam occ None in *) - (* let res = *) - (* match lam' with *) - (* | None -> None *) - (* | Some (prf, (car, rel, c1, c2)) -> *) - (* Some (resolve_morphism env sigma t *) - (* ~fnewt:unfold_all *) - (* (Lazy.force coq_all) [| x ; lam |] [| None; lam' |] *) - (* cstr evars) *) - (* in res, occ *) - (* else *) - | Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = @@ -1131,31 +1117,13 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = B. Barras' idea is to have a context of relations, of length 1, with Σ for gluing dependent relations and using projections to get them out. *) - (* | Lambda (n, t, b) when flags.under_lambdas -> *) - (* let n' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n in *) - (* let n'' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n' in *) - (* let n''' = name_app (fun id -> Tactics.fresh_id_in_env avoid id env) n'' in *) - (* let rel = new_cstr_evar cstr env (mkApp (Lazy.force coq_relation, [|t|])) in *) - (* let env' = Environ.push_rel_context [(n'',None,lift 2 rel);(n'',None,lift 1 t);(n', None, t)] env in *) - (* let b' = s env' avoid b (Typing.type_of env' (goalevars evars) (lift 2 b)) (unlift_cstr env (goalevars evars) cstr) evars in *) - (* (match b' with *) - (* | Some (Some r) -> *) - (* let prf = match r.rew_prf with *) - (* | RewPrf (rel, prf) -> *) - (* let rel = pointwise_or_dep_relation n' t r.rew_car rel in *) - (* let prf = mkLambda (n', t, prf) in *) - (* RewPrf (rel, prf) *) - (* | x -> x *) - (* in *) - (* Some (Some { r with *) - (* rew_prf = prf; *) - (* rew_car = mkProd (n, t, r.rew_car); *) - (* rew_from = mkLambda(n, t, r.rew_from); *) - (* rew_to = mkLambda (n, t, r.rew_to) }) *) - (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in + let unfresh = match n'.binder_name with + | Anonymous -> unfresh + | Name id -> Id.Set.add id unfresh + in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in @@ -1196,7 +1164,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Success r -> let case = mkCase (ci, lift 1 p, map_invert (lift 1) iv, mkRel 1, Array.map (lift 1) brs) in let res = make_leibniz_proof env case ty r in - state, Success (coerce env unfresh (prop,cstr) res) + state, Success (coerce env (prop,cstr) res) | Fail | Identity -> if Array.for_all (Int.equal 0) ci.ci_cstr_ndecls then let evars', eqty = app_poly_sort prop env evars coq_eq [| ty |] in @@ -1237,7 +1205,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = in let res = match res with - | Success r -> Success (coerce env unfresh (prop,cstr) r) + | Success r -> Success (coerce env (prop,cstr) r) | Fail | Identity -> res in state, res | _ -> state, Fail @@ -1671,9 +1639,9 @@ let cl_rewrite_clause l left2right occs clause = let cl_rewrite_clause_strat strat clause = cl_rewrite_clause_strat false strat clause -let apply_glob_constr c l2r occs = (); fun ({ state = () ; env = env } as input) -> +let apply_glob_constr ist c l2r occs = (); fun ({ state = () ; env = env } as input) -> let c sigma = - let (sigma, c) = Pretyping.understand_tcc env sigma c in + let (sigma, c) = Tacinterp.interp_open_constr ist env sigma c in (sigma, (c, NoBindings)) in let flags = general_rewrite_unif_flags () in @@ -1750,12 +1718,12 @@ let rec pr_strategy prc prr = function | StratEval r -> str "eval" ++ spc () ++ prr r | StratFold c -> str "fold" ++ spc () ++ prc c -let rec strategy_of_ast = function +let rec strategy_of_ast ist = function | StratId -> Strategies.id | StratFail -> Strategies.fail | StratRefl -> Strategies.refl | StratUnary (f, s) -> - let s' = strategy_of_ast s in + let s' = strategy_of_ast ist s in let f' = match f with | Subterms -> all_subterms | Subterm -> one_subterm @@ -1769,13 +1737,13 @@ let rec strategy_of_ast = function | Repeat -> Strategies.repeat in f' s' | StratBinary (f, s, t) -> - let s' = strategy_of_ast s in - let t' = strategy_of_ast t in + let s' = strategy_of_ast ist s in + let t' = strategy_of_ast ist t in let f' = match f with | Compose -> Strategies.seq | Choice -> Strategies.choice in f' s' t' - | StratConstr (c, b) -> { strategy = apply_glob_constr (fst c) b AllOccurrences } + | StratConstr (c, b) -> { strategy = apply_glob_constr ist c b AllOccurrences } | StratHints (old, id) -> if old then Strategies.old_hints id else Strategies.hints id | StratTerms l -> { strategy = (fun ({ state = () ; env } as input) -> @@ -1784,7 +1752,7 @@ let rec strategy_of_ast = function } | StratEval r -> { strategy = (fun ({ state = () ; env ; evars } as input) -> - let (sigma,r_interp) = Tacinterp.interp_redexp env (goalevars evars) r in + let (sigma,r_interp) = Tacinterp.interp_red_expr ist env (goalevars evars) r in (Strategies.reduce r_interp).strategy { input with evars = (sigma,cstrevars evars) }) } | StratFold c -> Strategies.fold_glob (fst c) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 60a66dd861..8e0ce183c2 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -62,7 +62,7 @@ type rewrite_result = type strategy -val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strategy +val strategy_of_ast : interp_sign -> (glob_constr_and_expr, glob_red_expr) strategy_ast -> strategy val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index ee28229cb7..4c1fe6417e 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -394,8 +394,13 @@ type appl = (* Values for interpretation *) type tacvalue = - | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t * - Name.t list * Tacexpr.glob_tactic_expr + | VFun of + appl * + Tacexpr.ltac_trace * + Loc.t option * (* when executing a global Ltac function: the location where this function was called *) + Val.t Id.Map.t * (* closure *) + Name.t list * (* binders *) + Tacexpr.glob_tactic_expr (* body *) | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index d58a76fe13..29e29044f1 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -31,21 +31,9 @@ type argument = Genarg.ArgT.any Extend.user_symbol (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - let atactic n = if n = 5 then Pcoq.Symbol.nterm Pltac.binder_tactic - else Pcoq.Symbol.nterml Pltac.tactic_expr (string_of_int n) + else Pcoq.Symbol.nterml Pltac.ltac_expr (string_of_int n) type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, _, 'a) Pcoq.Symbol.t -> entry_name @@ -70,28 +58,37 @@ let check_separator ?loc = function | Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.") let rec parse_user_entry ?loc s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-8)) None in + let open CString in + let matches pre suf s = + String.length s > (String.length pre + String.length suf) && + is_prefix pre s && is_suffix suf s + in + let basename pre suf s = + let plen = String.length pre in + String.sub s plen (String.length s - (plen + String.length suf)) + in + let tactic_len = String.length "tactic" in + if matches "ne_" "_list" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list" s) None in check_separator ?loc sep; Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 3 (l-12)) None in + else if matches "ne_" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "ne_" "_list_sep" s) None in Ulist1sep (entry, get_separator sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-5)) None in + else if matches "" "_list" s then + let entry = parse_user_entry ?loc (basename "" "_list" s) None in check_separator ?loc sep; Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-9)) None in + else if matches "" "_list_sep" s then + let entry = parse_user_entry ?loc (basename "" "_list_sep" s) None in Ulist0sep (entry, get_separator sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry ?loc (String.sub s 0 (l-4)) None in + else if matches "" "_opt" s then + let entry = parse_user_entry ?loc (basename "" "_opt" s) None in check_separator ?loc sep; Uopt entry - else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in + else if String.length s = tactic_len + 1 && is_prefix "tactic" s + && '5' >= s.[tactic_len] && s.[tactic_len] >= '0' then + let n = Char.code s.[tactic_len] - Char.code '0' in check_separator ?loc sep; Uentryl ("tactic", n) else @@ -119,7 +116,7 @@ let get_tactic_entry n = else if Int.equal n 5 then Pltac.binder_tactic, None else if 1<=n && n<5 then - Pltac.tactic_expr, Some (Gramlib.Gramext.Level (string_of_int n)) + Pltac.ltac_expr, Some (Gramlib.Gramext.Level (string_of_int n)) else user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^".")) @@ -159,7 +156,7 @@ let rec prod_item_of_symbol lev = function EntryName (Rawwit wit, Pcoq.Symbol.nterm (genarg_grammar wit)) | Extend.Uentryl (s, n) -> let ArgT.Any tag = s in - assert (coincide (ArgT.repr tag) "tactic" 0); + assert (CString.is_suffix "tactic" (ArgT.repr tag)); get_tacentry n lev (** Tactic grammar extensions *) @@ -386,7 +383,7 @@ let add_ml_tactic_notation name ~level ?deprecation prods = in List.iteri iter (List.rev prods); (* We call [extend_atomic_tactic] only for "basic tactics" (the ones - at tactic_expr level 0) *) + at ltac_expr level 0) *) if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) @@ -423,7 +420,7 @@ let create_ltac_quotation name cast (e, l) = in let action _ v _ _ _ loc = cast (Some loc, v) in let gram = (level, assoc, [Pcoq.Production.make rule action]) in - Pcoq.grammar_extend Pltac.tactic_arg {pos=None; data=[gram]} + Pcoq.grammar_extend Pltac.tactic_value {pos=None; data=[gram]} (** Command *) @@ -531,16 +528,40 @@ let print_ltacs () = let locatable_ltac = "Ltac" +let split_ltac_fun = function + | Tacexpr.TacFun (l,t) -> (l,t) + | t -> ([],t) + +let pr_ltac_fun_arg n = spc () ++ Name.print n + +let print_ltac_body qid tac = + let filter mp = + try Some (Nametab.shortest_qualid_of_module mp) + with Not_found -> None + in + let mods = List.map_filter filter tac.Tacenv.tac_redef in + let redefined = match mods with + | [] -> mt () + | mods -> + let redef = prlist_with_sep fnl pr_qualid mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in + let l,t = split_ltac_fun tac.Tacenv.tac_body in + hv 2 ( + hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++ + prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") + ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined + let () = let open Prettyp in - let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in - let locate_all = Tacenv.locate_extended_all_tactic in - let shortest_qualid = Tacenv.shortest_qualid_of_tactic in - let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in - let print kn = - let qid = qualid_of_path (Tacenv.path_of_tactic kn) in - Tacintern.print_ltac qid - in + let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in + let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in + let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in + let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in + let print (qid,kn) = + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + print_ltac_body qid tac in let about = name in register_locatable locatable_ltac { locate; @@ -554,14 +575,25 @@ let () = let print_located_tactic qid = Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid) +let print_ltac id = + try + let kn = Tacenv.locate_tactic id in + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + print_ltac_body id tac + with + Not_found -> + user_err ~hdr:"print_ltac" + (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") + (** Grammar *) let () = let entries = [ - AnyEntry Pltac.tactic_expr; + AnyEntry Pltac.ltac_expr; AnyEntry Pltac.binder_tactic; AnyEntry Pltac.simple_tactic; - AnyEntry Pltac.tactic_arg; + AnyEntry Pltac.tactic_value; ] in register_grammars_by_name "tactic" entries diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 6ee3ce091b..fc9ab54eba 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -69,6 +69,9 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +val print_ltac : Libnames.qualid -> Pp.t +(** Display the definition of a tactic. *) + (** {5 Low-level registering of tactics} *) type (_, 'a) ml_ty_sig = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9c3b05fdf1..47f1d3bf66 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -769,38 +769,6 @@ let glob_tactic_env l env x = (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x -let split_ltac_fun = function - | TacFun (l,t) -> (l,t) - | t -> ([],t) - -let pr_ltac_fun_arg n = spc () ++ Name.print n - -let print_ltac id = - try - let kn = Tacenv.locate_tactic id in - let entries = Tacenv.ltac_entries () in - let tac = KNmap.find kn entries in - let filter mp = - try Some (Nametab.shortest_qualid_of_module mp) - with Not_found -> None - in - let mods = List.map_filter filter tac.Tacenv.tac_redef in - let redefined = match mods with - | [] -> mt () - | mods -> - let redef = prlist_with_sep fnl pr_qualid mods in - fnl () ++ str "Redefined by:" ++ fnl () ++ redef - in - let l,t = split_ltac_fun tac.Tacenv.tac_body in - hv 2 ( - hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ - prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined - with - Not_found -> - user_err ~hdr:"print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") - (** Registering *) let lift intern = (); fun ist x -> (ist, intern ist x) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 22ec15566b..f779aa470c 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -(** printing *) -val print_ltac : Libnames.qualid -> Pp.t - (** Reduction expressions *) val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..3d734d3a66 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -153,11 +153,15 @@ let add_extra_loc loc extra = match loc with | None -> extra | Some loc -> TacStore.set extra f_loc loc -let add_loc loc ist = +let extract_loc ist = TacStore.get ist.extra f_loc + +let ensure_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 + | Some loc -> + match extract_loc ist with + | None -> { ist with extra = TacStore.set ist.extra f_loc loc } + | Some _ -> ist let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -1175,7 +1179,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 {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v) + | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_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)} -> @@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in + (* We call a global ltac reference: add a loc on its executation only if not + already in another global reference *) + let ist = ensure_loc loc ist in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false - (catch_error_tac_loc (* interp *) loc false trace - (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r))) + (catch_error_tac_loc (* loc for interpretation *) loc false trace + (val_interp ~appl ist (Tacenv.interp_ltac r))) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1325,7 +1332,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 (add_loc loc ist) body)) >>= fun v -> + (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1997,7 +2004,7 @@ let interp_tac_gen lfun avoid_ids debug t = let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* MUST be marshallable! *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } @@ -2019,7 +2026,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 01d7306c9d..a74f4592f7 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -77,6 +77,9 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic (** Interprets redexp arguments *) +val interp_red_expr : interp_sign -> Environ.env -> Evd.evar_map -> glob_red_expr -> Evd.evar_map * red_expr + +(** Interprets redexp arguments from a raw one *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) @@ -126,12 +129,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t -> val interp : raw_tactic_expr -> unit Proofview.tactic (** Hides interpretation for pretty-print *) -type tactic_expr = { +type ltac_expr = { global: bool; ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr ComTactic.tactic_interpreter +val hide_interp : ltac_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 3360a9a51c..21178a64a5 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -36,10 +36,8 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct module Table = Hashtbl.Make (Key) exception InvalidTableFormat - exception UnboundTable - type mode = Closed | Open - type 'a t = {outch : out_channel; mutable status : mode; htbl : 'a Table.t} + type 'a t = {outch : out_channel; htbl : 'a Table.t} (* XXX: Move to Fun.protect once in Ocaml 4.08 *) let fun_protect ~(finally : unit -> unit) work = @@ -118,7 +116,6 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct close_in_noerr inch; { outch = out_channel_of_descr (openfile f [O_WRONLY; O_APPEND; O_CREAT] 0o666) - ; status = Open ; htbl } with InvalidTableFormat -> (* The file is corrupted *) @@ -131,24 +128,20 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct (fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing]) htbl; flush outch); - {outch; status = Open; htbl} + {outch; htbl} let add t k e = - let {outch; status; htbl = tbl} = t in - if status == Closed then raise UnboundTable - else - let fd = descr_of_out_channel outch in - Table.add tbl k e; - do_under_lock Write fd (fun _ -> - Marshal.to_channel outch (k, e) [Marshal.No_sharing]; - flush outch) + let {outch; htbl = tbl} = t in + let fd = descr_of_out_channel outch in + Table.add tbl k e; + do_under_lock Write fd (fun _ -> + Marshal.to_channel outch (k, e) [Marshal.No_sharing]; + flush outch) let find t k = - let {outch; status; htbl = tbl} = t in - if status == Closed then raise UnboundTable - else - let res = Table.find tbl k in - res + let {outch; htbl = tbl} = t in + let res = Table.find tbl k in + res let memo cache f = let tbl = lazy (try Some (open_in cache) with _ -> None) in diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index d464ec4c06..61f90608b1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -100,7 +100,7 @@ let rec make_form env sigma atom_env term = | Cast(a,_,_) -> make_form env sigma atom_env a | Ind (ind, _) -> - if Names.eq_ind ind (fst (Lazy.force li_False)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_False)) then Bot else make_atom atom_env (normalize term) @@ -108,11 +108,11 @@ let rec make_form env sigma atom_env term = begin try let ind, _ = destInd sigma hd in - if Names.eq_ind ind (fst (Lazy.force li_and)) then + if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_and)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Conjunct (fa,fb) - else if Names.eq_ind ind (fst (Lazy.force li_or)) then + else if Names.Ind.CanOrd.equal ind (fst (Lazy.force li_or)) then let fa = make_form env sigma atom_env argv.(0) in let fb = make_form env sigma atom_env argv.(1) in Disjunct (fa,fb) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 38b26d06b9..a7ebd5f9f5 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -240,7 +240,7 @@ let strip_unfold_term _ ((sigma, t) as p) kt = match EConstr.kind sigma t with let same_proj sigma t1 t2 = match EConstr.kind sigma t1, EConstr.kind sigma t2 with - | Proj(c1,_), Proj(c2, _) -> Projection.equal c1 c2 + | Proj(c1,_), Proj(c2, _) -> Projection.CanOrd.equal c1 c2 | _ -> false let all_ok _ _ = true diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 7b584b5159..ccdf5fa68e 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -100,7 +100,7 @@ ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtacarg; - ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]]; + ssrtacarg: [[ tac = ltac_expr LEVEL "5" -> { tac } ]]; END (* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *) @@ -108,7 +108,7 @@ ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma } END GRAMMAR EXTEND Gram GLOBAL: ssrtac3arg; - ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]]; + ssrtac3arg: [[ tac = ltac_expr LEVEL "3" -> { tac } ]]; END { @@ -350,7 +350,7 @@ let interp_index ist gl idx = | Some c -> let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc (None, []) with - | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n -> + | Constrexpr.Number n, _ when NumTok.Signed.is_int n -> int_of_string (NumTok.Signed.to_string n) | _ -> raise Not_found end @@ -1337,7 +1337,7 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde GRAMMAR EXTEND Gram GLOBAL: ssrbinder; ssrbinder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; @@ -1594,18 +1594,18 @@ GRAMMAR EXTEND Gram | n = Prim.natural -> { ArgArg (check_index ~loc n) } ] ]; ssrswap: [[ IDENT "first" -> { loc, true } | IDENT "last" -> { loc, false } ]]; - ssrorelse: [[ "||"; tac = tactic_expr LEVEL "2" -> { tac } ]]; + ssrorelse: [[ "||"; tac = ltac_expr LEVEL "2" -> { tac } ]]; ssrseqarg: [ [ arg = ssrswap -> { noindex, swaptacarg arg } | i = ssrseqidx; tac = ssrortacarg; def = OPT ssrorelse -> { i, (tac, def) } | i = ssrseqidx; arg = ssrswap -> { i, swaptacarg arg } - | tac = tactic_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } + | tac = ltac_expr LEVEL "3" -> { noindex, (mk_hint tac, None) } ] ]; END { -let tactic_expr = Pltac.tactic_expr +let ltac_expr = Pltac.ltac_expr } @@ -1688,9 +1688,9 @@ let tclintros_expr ?loc tac ipats = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "1" [ RIGHTA - [ tac = tactic_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } + GLOBAL: ltac_expr; + ltac_expr: LEVEL "1" [ RIGHTA + [ tac = ltac_expr; intros = ssrintros_ne -> { tclintros_expr ~loc tac intros } ] ]; END @@ -1704,9 +1704,9 @@ END (* (Removing user-specified parentheses is dubious anyway). *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - ssrparentacarg: [[ "("; tac = tactic_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; - tactic_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; + GLOBAL: ltac_expr; + ssrparentacarg: [[ "("; tac = ltac_expr; ")" -> { CAst.make ~loc (Tacexp tac) } ]]; + ltac_expr: LEVEL "0" [[ arg = ssrparentacarg -> { TacArg arg } ]]; END (** The internal "done" and "ssrautoprop" tactics. *) @@ -1741,7 +1741,7 @@ let tclBY tac = Tacticals.New.tclTHEN tac (donetac ~-1) (* The latter two are used in forward-chaining tactics (have, suffice, wlog) *) (* and subgoal reordering tacticals (; first & ; last), respectively. *) -(* Force use of the tactic_expr parsing entry, to rule out tick marks. *) +(* Force use of the ltac_expr parsing entry, to rule out tick marks. *) (** The "by" tactical. *) @@ -1782,12 +1782,12 @@ let ssrdotac_expr ?loc n m tac clauses = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssrdotac: [ - [ tac = tactic_expr LEVEL "3" -> { mk_hint tac } + [ tac = ltac_expr LEVEL "3" -> { mk_hint tac } | tacs = ssrortacarg -> { tacs } ] ]; - tactic_expr: LEVEL "3" [ RIGHTA + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "do"; m = ssrmmod; tac = ssrdotac; clauses = ssrclauses -> { ssrdotac_expr ~loc noindex m tac clauses } | IDENT "do"; tac = ssrortacarg; clauses = ssrclauses -> @@ -1833,20 +1833,20 @@ let tclseq_expr ?loc tac dir arg = } GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; + GLOBAL: ltac_expr; ssr_first: [ [ tac = ssr_first; ipats = ssrintros_ne -> { tclintros_expr ~loc tac ipats } - | "["; tacl = LIST0 tactic_expr SEP "|"; "]" -> { TacFirst tacl } + | "["; tacl = LIST0 ltac_expr SEP "|"; "]" -> { TacFirst tacl } ] ]; ssr_first_else: [ [ tac1 = ssr_first; tac2 = ssrorelse -> { TacOrelse (tac1, tac2) } | tac = ssr_first -> { tac } ]]; - tactic_expr: LEVEL "4" [ LEFTA - [ tac1 = tactic_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> + ltac_expr: LEVEL "4" [ LEFTA + [ tac1 = ltac_expr; ";"; IDENT "first"; tac2 = ssr_first_else -> { TacThen (tac1, tac2) } - | tac = tactic_expr; ";"; IDENT "first"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "first"; arg = ssrseqarg -> { tclseq_expr ~loc tac L2R arg } - | tac = tactic_expr; ";"; IDENT "last"; arg = ssrseqarg -> + | tac = ltac_expr; ";"; IDENT "last"; arg = ssrseqarg -> { tclseq_expr ~loc tac R2L arg } ] ]; END @@ -1894,7 +1894,8 @@ let has_occ ((_, occ), _) = occ <> None let gens_sep = function [], [] -> mt | _ -> spc let pr_dgens pr_gen (gensl, clr) = - let prgens s gens = str s ++ pr_list spc pr_gen gens in + let prgens s gens = + if CList.is_empty gens then mt () else str s ++ pr_list spc pr_gen gens in let prdeps deps = prgens ": " deps ++ spc () ++ str "/" in match gensl with | [deps; []] -> prdeps deps ++ pr_clear pr_spc clr @@ -2194,7 +2195,7 @@ END let pr_ssrcongrarg _ _ _ ((n, f), dgens) = (if n <= 0 then mt () else str " " ++ int n) ++ - str " " ++ pr_term f ++ pr_dgens pr_gen dgens + pr_term f ++ pr_dgens pr_gen dgens } @@ -2447,8 +2448,8 @@ END (* The standard TACTIC EXTEND does not work for abstract *) GRAMMAR EXTEND Gram - GLOBAL: tactic_expr; - tactic_expr: LEVEL "3" + GLOBAL: ltac_expr; + ltac_expr: LEVEL "3" [ RIGHTA [ IDENT "abstract"; gens = ssrdgens -> { ssrtac_expr ~loc "abstract" [Tacexpr.TacGeneric (None, Genarg.in_gen (Genarg.rawwit wit_ssrdgens) gens)] } ]]; diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index e231ab1f87..ab36d4fc7c 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -75,11 +75,14 @@ let pr_hyp (SsrHyp (_, id)) = Id.print id let pr_hyps = pr_list pr_spc pr_hyp let pr_occ = function - | Some (true, occ) -> str "{-" ++ pr_list pr_spc int occ ++ str "}" - | Some (false, occ) -> str "{+" ++ pr_list pr_spc int occ ++ str "}" + | Some (true, occ) -> + if CList.is_empty occ then mt () else str "{-" ++ pr_list pr_spc int occ ++ str "}" + | Some (false, occ) -> + if CList.is_empty occ then mt () else str "{+" ++ pr_list pr_spc int occ ++ str "}" | None -> str "{}" -let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}" +let pr_clear_ne clr = + if CList.is_empty clr then mt () else str "{" ++ pr_hyps clr ++ str "}" let pr_clear sep clr = sep () ++ pr_clear_ne clr let pr_dir = function L2R -> str "->" | R2L -> str "<-" diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 4a907b2795..99cf197b78 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -85,7 +85,7 @@ let mk_pat c (na, t) = (c, na, t) GRAMMAR EXTEND Gram GLOBAL: binder_constr; - ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> { mk_rtype t } ]]; + ssr_rtype: [[ "return"; t = term LEVEL "100" -> { mk_rtype t } ]]; ssr_mpat: [[ p = pattern -> { [[p]] } ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> { mp, mk_ctype mp t, rt } @@ -96,9 +96,9 @@ GRAMMAR EXTEND Gram ssr_elsepat: [[ "else" -> { [[CAst.make ~loc @@ CPatAtom None]] } ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> { CAst.make ~loc (mp, c) } ]]; binder_constr: [ - [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> + [ "if"; c = term LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in CAst.make ~loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) } - | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> + | "if"; c = term LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> { let b1, ct, rt = db1 in let b1, b2 = let open CAst in let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in @@ -119,7 +119,7 @@ END GRAMMAR EXTEND Gram GLOBAL: closed_binder; closed_binder: [ - [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> + [ ["of" -> { () } | "&" -> { () } ]; c = term LEVEL "99" -> { [CLocalAssum ([CAst.make ~loc Anonymous], Default Explicit, c)] } ] ]; END @@ -304,15 +304,6 @@ END { - let warn_search_moved_enabled = ref true - let warn_search_moved = CWarnings.create ~name:"ssr-search-moved" - ~category:"deprecated" ~default:CWarnings.Enabled - (fun () -> - (Pp.strbrk - "SSReflect's Search command has been moved to the \ - ssrsearch module; please Require that module if you \ - still want to use SSReflect's Search command")) - open G_vernac } @@ -322,7 +313,6 @@ GRAMMAR EXTEND Gram query_command: [ [ IDENT "Search"; s = search_query; l = search_queries; "." -> { let (sl,m) = l in - if !warn_search_moved_enabled then warn_search_moved (); fun g -> Vernacexpr.VernacSearch (Vernacexpr.Search (s::sl),g, m) } ] ] diff --git a/plugins/ssr/ssrvernac.mli b/plugins/ssr/ssrvernac.mli index 93339313f0..327a2d4660 100644 --- a/plugins/ssr/ssrvernac.mli +++ b/plugins/ssr/ssrvernac.mli @@ -9,5 +9,3 @@ (************************************************************************) (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) - -val warn_search_moved_enabled : bool ref diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index cdd15acb0d..bd514f15d5 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -463,8 +463,8 @@ let nb_cs_proj_args pc f u = try match kind f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) - | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f - | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f + | Const (c',_) when Constant.CanOrd.equal c' pc -> nargs_of_proj u.up_f + | Proj (c',_) when Constant.CanOrd.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (fst @@ destRef f)) | _ -> -1 with Not_found -> -1 @@ -508,7 +508,7 @@ let filter_upat i0 f n u fpats = let () = if !i0 < np then i0 := n in (u, np) :: fpats let eq_prim_proj c t = match kind t with - | Proj(p,_) -> Constant.equal (Projection.constant p) c + | Proj(p,_) -> Constant.CanOrd.equal (Projection.constant p) c | _ -> false let filter_upat_FO i0 f n u fpats = diff --git a/plugins/ssrsearch/g_search.mlg b/plugins/ssrsearch/g_search.mlg index 5e002e09cc..54fdea0860 100644 --- a/plugins/ssrsearch/g_search.mlg +++ b/plugins/ssrsearch/g_search.mlg @@ -301,10 +301,6 @@ let ssrdisplaysearch gr env t = let pr_res = pr_global gr ++ str ":" ++ spc () ++ pr_lconstr_env env Evd.empty t in Feedback.msg_notice (hov 2 pr_res ++ fnl ()) -(* Remove the warning entirely when this plugin is loaded. *) -let _ = - Ssreflect_plugin.Ssrvernac.warn_search_moved_enabled := false - let deprecated_search = CWarnings.create ~name:"deprecated-ssr-search" diff --git a/plugins/syntax/dune b/plugins/syntax/dune index b395695c8a..f930fc265a 100644 --- a/plugins/syntax/dune +++ b/plugins/syntax/dune @@ -1,22 +1,8 @@ (library - (name numeral_notation_plugin) - (public_name coq.plugins.numeral_notation) - (synopsis "Coq numeral notation plugin") - (modules g_numeral numeral) - (libraries coq.vernac)) - -(library - (name string_notation_plugin) - (public_name coq.plugins.string_notation) - (synopsis "Coq string notation plugin") - (modules g_string string_notation) - (libraries coq.vernac)) - -(library - (name r_syntax_plugin) - (public_name coq.plugins.r_syntax) - (synopsis "Coq syntax plugin: reals") - (modules r_syntax) + (name number_string_notation_plugin) + (public_name coq.plugins.number_string_notation) + (synopsis "Coq number and string notation plugin") + (modules g_number_string string_notation number) (libraries coq.vernac)) (library @@ -33,4 +19,4 @@ (modules float_syntax) (libraries coq.vernac)) -(coq.pp (modules g_numeral g_string)) +(coq.pp (modules g_number_string)) diff --git a/plugins/syntax/g_number_string.mlg b/plugins/syntax/g_number_string.mlg new file mode 100644 index 0000000000..c8badd238d --- /dev/null +++ b/plugins/syntax/g_number_string.mlg @@ -0,0 +1,110 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +DECLARE PLUGIN "number_string_notation_plugin" + +{ + +open Notation +open Number +open String_notation +open Pp +open Names +open Stdarg +open Pcoq.Prim + +let pr_number_after = function + | Nop -> mt () + | Warning n -> str "warning after " ++ NumTok.UnsignedNat.print n + | Abstract n -> str "abstract after " ++ NumTok.UnsignedNat.print n + +let pr_deprecated_number_modifier m = str "(" ++ pr_number_after m ++ str ")" + +let warn_deprecated_numeral_notation = + CWarnings.create ~name:"numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Numeral Notation is deprecated, please use Number Notation instead.") + +let pr_number_string_mapping (b, n, n') = + if b then + str "[" ++ Libnames.pr_qualid n ++ str "]" ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + else + Libnames.pr_qualid n ++ spc () ++ str "=>" ++ spc () + ++ Libnames.pr_qualid n' + +let pr_number_string_via (n, l) = + str "via " ++ Libnames.pr_qualid n ++ str " mapping [" + ++ prlist_with_sep pr_comma pr_number_string_mapping l ++ str "]" + +let pr_number_modifier = function + | After a -> pr_number_after a + | Via nl -> pr_number_string_via nl + +let pr_number_options l = + str "(" ++ prlist_with_sep pr_comma pr_number_modifier l ++ str ")" + +let pr_string_option l = + str "(" ++ pr_number_string_via l ++ str ")" + +} + +VERNAC ARGUMENT EXTEND deprecated_number_modifier + PRINTED BY { pr_deprecated_number_modifier } +| [ ] -> { Nop } +| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } +| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } +END + +VERNAC ARGUMENT EXTEND number_string_mapping + PRINTED BY { pr_number_string_mapping } +| [ reference(n) "=>" reference(n') ] -> { false, n, n' } +| [ "[" reference(n) "]" "=>" reference(n') ] -> { true, n, n' } +END + +VERNAC ARGUMENT EXTEND number_string_via + PRINTED BY { pr_number_string_via } +| [ "via" reference(n) "mapping" "[" ne_number_string_mapping_list_sep(l, ",") "]" ] -> { n, l } +END + +VERNAC ARGUMENT EXTEND number_modifier + PRINTED BY { pr_number_modifier } +| [ "warning" "after" bignat(waft) ] -> { After (Warning (NumTok.UnsignedNat.of_string waft)) } +| [ "abstract" "after" bignat(n) ] -> { After (Abstract (NumTok.UnsignedNat.of_string n)) } +| [ number_string_via(v) ] -> { Via v } +END + +VERNAC ARGUMENT EXTEND number_options + PRINTED BY { pr_number_options } +| [ "(" ne_number_modifier_list_sep(l, ",") ")" ] -> { l } +END + +VERNAC ARGUMENT EXTEND string_option + PRINTED BY { pr_string_option } +| [ "(" number_string_via(v) ")" ] -> { v } +END + +VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF + | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) number_options_opt(nl) ":" + ident(sc) ] -> + + { vernac_number_notation (Locality.make_module_locality locality) ty f g (Option.default [] nl) (Id.to_string sc) } + | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":" + ident(sc) deprecated_number_modifier(o) ] -> + + { warn_deprecated_numeral_notation (); + vernac_number_notation (Locality.make_module_locality locality) ty f g [After o] (Id.to_string sc) } +END + +VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF + | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) string_option_opt(o) ":" + ident(sc) ] -> + { vernac_string_notation (Locality.make_module_locality locality) ty f g o (Id.to_string sc) } +END diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg deleted file mode 100644 index c030925ea9..0000000000 --- a/plugins/syntax/g_numeral.mlg +++ /dev/null @@ -1,51 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) - -DECLARE PLUGIN "numeral_notation_plugin" - -{ - -open Notation -open Numeral -open Pp -open Names -open Stdarg -open Pcoq.Prim - -let pr_numnot_option = function - | Nop -> mt () - | 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 - PRINTED BY { pr_numnot_option } -| [ ] -> { Nop } -| [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) } -| [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) } -END - -VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF - | #[ 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 diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg deleted file mode 100644 index 788f9e011d..0000000000 --- a/plugins/syntax/g_string.mlg +++ /dev/null @@ -1,25 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) - -DECLARE PLUGIN "string_notation_plugin" - -{ - -open String_notation -open Names -open Stdarg - -} - -VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF - | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":" - ident(sc) ] -> - { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) } -END diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml index 5f4db8e800..b14b02f3bb 100644 --- a/plugins/syntax/int63_syntax.ml +++ b/plugins/syntax/int63_syntax.ml @@ -43,6 +43,7 @@ let _ = let id_int63 = Nametab.locate q_id_int63 in let o = { to_kind = Int63, Direct; to_ty = id_int63; + to_post = [||]; of_kind = Int63, Direct; of_ty = id_int63; ty_name = q_int63; @@ -50,7 +51,7 @@ let _ = enable_prim_token_interpretation { pt_local = false; pt_scope = int63_scope; - pt_interp_info = NumeralNotation o; + pt_interp_info = NumberNotation o; pt_required = (int63_path, int63_module); pt_refs = []; pt_in_match = false }) diff --git a/plugins/syntax/number.ml b/plugins/syntax/number.ml new file mode 100644 index 0000000000..89d757a72a --- /dev/null +++ b/plugins/syntax/number.ml @@ -0,0 +1,505 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +open Pp +open Util +open Names +open Libnames +open Constrexpr +open Constrexpr_ops +open Notation + +module CSet = CSet.Make (Constr) +module CMap = CMap.Make (Constr) + +(** * Number notation *) + +type number_string_via = qualid * (bool * qualid * qualid) list +type number_option = + | After of numnot_option + | Via of number_string_via + +let warn_abstract_large_num_no_op = + CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" + (fun f -> + strbrk "The 'abstract after' directive has no effect when " ++ + strbrk "the parsing function (" ++ + Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ + strbrk "option type.") + +let get_constructors ind = + let mib,oib = Global.lookup_inductive ind in + let mc = oib.Declarations.mind_consnames in + Array.to_list + (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) + +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 + | GlobRef.IndRef i -> i + | _ -> raise Not_found + +let locate_z () = + 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_number () = + let dint = "num.int.type" in + let duint = "num.uint.type" in + let dec = "num.decimal.type" in + let hint = "num.hexadecimal_int.type" in + let huint = "num.hexadecimal_uint.type" in + let hex = "num.hexadecimal.type" in + let int = "num.num_int.type" in + let uint = "num.num_uint.type" in + let num = "num.number.type" in + if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec + && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex + && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num + then + let q_dint = qualid_of_ref dint in + let q_duint = qualid_of_ref duint in + let q_dec = qualid_of_ref dec in + let q_hint = qualid_of_ref hint in + let q_huint = qualid_of_ref huint in + let q_hex = qualid_of_ref hex in + let q_int = qualid_of_ref int in + let q_uint = qualid_of_ref uint in + let q_num = qualid_of_ref num in + let int_ty = { + dec_int = unsafe_locate_ind q_dint; + dec_uint = unsafe_locate_ind q_duint; + hex_int = unsafe_locate_ind q_hint; + hex_uint = unsafe_locate_ind q_huint; + int = unsafe_locate_ind q_int; + uint = unsafe_locate_ind q_uint; + } in + let num_ty = { + int = int_ty; + decimal = unsafe_locate_ind q_dec; + hexadecimal = unsafe_locate_ind q_hex; + number = unsafe_locate_ind q_num; + } in + Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, + num_ty, mkRefC q_num, mkRefC q_dec) + else None + +let locate_int63 () = + let int63n = "num.int63.type" in + if Coqlib.has_ref int63n + then + let q_int63 = qualid_of_ref int63n in + Some (mkRefC q_int63) + else None + +let has_type env sigma f ty = + let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in + try let _ = Constrintern.interp_constr env sigma c in true + with Pretype_errors.PretypeError _ -> false + +let type_error_to f ty = + CErrors.user_err + (pr_qualid f ++ str " should go from Number.int to " ++ + pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ + fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + +let type_error_of g ty = + CErrors.user_err + (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ + str " to Number.int or (option Number.int)." ++ fnl () ++ + str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).") + +let warn_deprecated_decimal = + CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" + (fun () -> + strbrk "Deprecated Number Notation for Decimal.uint, \ + Decimal.int or Decimal.decimal. Use Number.uint, \ + Number.int or Number.number respectively.") + +let error_params ind = + CErrors.user_err + (str "Wrong number of parameters for inductive" ++ spc () + ++ Printer.pr_global (GlobRef.IndRef ind) ++ str ".") + +let remapping_error ?loc ty ty' ty'' = + CErrors.user_err ?loc + (Printer.pr_global ty + ++ str " was already mapped to" ++ spc () ++ Printer.pr_global ty' + ++ str " and cannot be remapped to" ++ spc () ++ Printer.pr_global ty'' + ++ str ".") + +let error_missing c = + CErrors.user_err + (str "Missing mapping for constructor " ++ Printer.pr_global c ++ str ".") + +let pr_constr env sigma c = + let c = Constrextern.extern_constr env sigma (EConstr.of_constr c) in + Ppconstr.pr_constr_expr env sigma c + +let warn_via_remapping = + CWarnings.create ~name:"via-type-remapping" ~category:"numbers" + (fun (env, sigma, ty, ty', ty'') -> + let constr = pr_constr env sigma in + constr ty ++ str " was already mapped to" ++ spc () ++ constr ty' + ++ str ", mapping it also to" ++ spc () ++ constr ty'' + ++ str " might yield ill typed terms when using the notation.") + +let warn_via_type_mismatch = + CWarnings.create ~name:"via-type-mismatch" ~category:"numbers" + (fun (env, sigma, g, g', exp, actual) -> + let constr = pr_constr env sigma in + str "Type of" ++ spc() ++ Printer.pr_global g + ++ str " seems incompatible with the type of" ++ spc () + ++ Printer.pr_global g' ++ str "." ++ spc () + ++ str "Expected type is: " ++ constr exp ++ spc () + ++ str "instead of " ++ constr actual ++ str "." ++ spc () + ++ str "This might yield ill typed terms when using the notation.") + +let multiple_via_error () = + CErrors.user_err (Pp.str "Multiple 'via' options.") + +let multiple_after_error () = + CErrors.user_err (Pp.str "Multiple 'warning after' or 'abstract after' options.") + +let via_abstract_error () = + CErrors.user_err (Pp.str "'via' and 'abstract' cannot be used together.") + +let locate_global_sort_inductive_or_constant sigma qid = + let locate_sort qid = + match Nametab.locate_extended qid with + | Globnames.TrueGlobal _ -> raise Not_found + | Globnames.SynDef kn -> + match Syntax_def.search_syntactic_definition kn with + | [], Notation_term.NSort r -> + let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family r) in + sigma,Constr.mkSort c + | _ -> raise Not_found in + try locate_sort qid + with Not_found -> + match Smartlocate.global_with_alias qid with + | GlobRef.IndRef i -> sigma, Constr.mkInd i + | _ -> sigma, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +let locate_global_constructor_inductive_or_constant qid = + let g = Smartlocate.global_with_alias qid in + match g with + | GlobRef.ConstructRef c -> g, Constr.mkConstruct c + | GlobRef.IndRef i -> g, Constr.mkInd i + | _ -> g, Constr.mkConst (Smartlocate.global_constant_with_alias qid) + +(* [get_type env sigma c] retrieves the type of [c] and returns a pair + [l, t] such that [c : l_0 -> ... -> l_n -> t]. *) +let get_type env sigma c = + (* inspired from [compute_implicit_names] in "interp/impargs.ml" *) + let rec aux env acc t = + let t = Reductionops.whd_all env sigma t in + match EConstr.kind sigma t with + | Constr.Prod (na, a, b) -> + let a = Reductionops.whd_all env sigma a in + let rel = Context.Rel.Declaration.LocalAssum (na, a) in + aux (EConstr.push_rel rel env) ((na, a) :: acc) b + | _ -> List.rev acc, t in + let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let l, t = aux env [] t in + List.map (fun (na, a) -> na, EConstr.Unsafe.to_constr a) l, + EConstr.Unsafe.to_constr t + +(* [elaborate_to_post_params env sigma ty_ind params] builds the + [to_post] translation (c.f., interp/notation.mli) for the numeral + notation to parse/print type [ty_ind]. This translation is the + identity ([ToPostCopy]) except that it checks ([ToPostCheck]) that + the parameters of the inductive type [ty_ind] match the ones given + in [params]. *) +let elaborate_to_post_params env sigma ty_ind params = + let to_post_for_constructor indc = + let sigma, c = match indc with + | GlobRef.ConstructRef c -> + let sigma,c = Evd.fresh_constructor_instance env sigma c in + sigma, Constr.mkConstructU c + | _ -> assert false in (* c.f. get_constructors *) + let args, t = get_type env sigma c in + let params_indc = match Constr.kind t with + | Constr.App (_, a) -> Array.to_list a | _ -> [] in + let sz = List.length args in + let a = Array.make sz ToPostCopy in + if List.length params <> List.length params_indc then error_params ty_ind; + List.iter2 (fun param param_indc -> + match param, Constr.kind param_indc with + | Some p, Constr.Rel i when i <= sz -> a.(sz - i) <- ToPostCheck p + | _ -> ()) + params params_indc; + indc, indc, Array.to_list a in + let pt_refs = get_constructors ty_ind in + let to_post_0 = List.map to_post_for_constructor pt_refs in + let to_post = + let only_copy (_, _, args) = List.for_all ((=) ToPostCopy) args in + if (List.for_all only_copy to_post_0) then [||] else [|to_post_0|] in + to_post, pt_refs + +(* [elaborate_to_post_via env sigma ty_name ty_ind l] builds the [to_post] + translation (c.f., interp/notation.mli) for the number notation to + parse/print type [ty_name] through the inductive [ty_ind] according + to the pairs [constant, constructor] in the list [l]. *) +let elaborate_to_post_via env sigma ty_name ty_ind l = + let sigma, ty_name = + locate_global_sort_inductive_or_constant sigma ty_name in + let ty_ind = Constr.mkInd ty_ind in + (* Retrieve constants and constructors mappings and their type. + For each constant [cnst] and inductive constructor [indc] in [l], retrieve: + * its location: [lcnst] and [lindc] + * its GlobRef: [cnst] and [indc] + * its type: [tcnst] and [tindc] (decomposed in product by [get_type] above) + * [impls] are the implicit arguments of [cnst] *) + let l = + let read (consider_implicits, cnst, indc) = + let lcnst, lindc = cnst.CAst.loc, indc.CAst.loc in + let cnst, ccnst = locate_global_constructor_inductive_or_constant cnst in + let indc, cindc = + let indc = Smartlocate.global_constructor_with_alias indc in + GlobRef.ConstructRef indc, Constr.mkConstruct indc in + let get_type_wo_params c = + (* ignore parameters of inductive types *) + let rm_params c = match Constr.kind c with + | Constr.App (c, _) when Constr.isInd c -> c + | _ -> c in + let lc, tc = get_type env sigma c in + List.map (fun (n, c) -> n, rm_params c) lc, rm_params tc in + let tcnst, tindc = get_type_wo_params ccnst, get_type_wo_params cindc in + let impls = + if not consider_implicits then [] else + Impargs.(select_stronger_impargs (implicits_of_global cnst)) in + lcnst, cnst, tcnst, lindc, indc, tindc, impls in + List.map read l in + let eq_indc indc (_, _, _, _, indc', _, _) = GlobRef.equal indc indc' in + (* Collect all inductive types involved. + That is [ty_ind] and all final codomains of [tindc] above. *) + let inds = + List.fold_left (fun s (_, _, _, _, _, tindc, _) -> CSet.add (snd tindc) s) + (CSet.singleton ty_ind) l in + (* And for each inductive, retrieve its constructors. *) + let constructors = + CSet.fold (fun ind m -> + let inductive, _ = Constr.destInd ind in + CMap.add ind (get_constructors inductive) m) + inds CMap.empty in + (* Error if one [constructor] in some inductive in [inds] + doesn't appear exactly once in [l] *) + let _ = (* check_for duplicate constructor and error *) + List.fold_left (fun already_seen (_, cnst, _, loc, indc, _, _) -> + try + let cnst' = List.assoc_f GlobRef.equal indc already_seen in + remapping_error ?loc indc cnst' cnst + with Not_found -> (indc, cnst) :: already_seen) + [] l in + let () = (* check for missing constructor and error *) + CMap.iter (fun _ -> + List.iter (fun cstr -> + if not (List.exists (eq_indc cstr) l) then error_missing cstr)) + constructors in + (* Perform some checks on types and warn if they look strange. + These checks are neither sound nor complete, so we only warn. *) + let () = + (* associate inductives to types, and check that this mapping is one to one + and maps [ty_ind] to [ty_name] *) + let ind2ty, ty2ind = + let add loc ckey cval m = + match CMap.find_opt ckey m with + | None -> CMap.add ckey cval m + | Some old_cval -> + if not (Constr.equal old_cval cval) then + warn_via_remapping ?loc (env, sigma, ckey, old_cval, cval); + m in + List.fold_left + (fun (ind2ty, ty2ind) (lcnst, _, (_, tcnst), lindc, _, (_, tindc), _) -> + add lcnst tindc tcnst ind2ty, add lindc tcnst tindc ty2ind) + CMap.(singleton ty_ind ty_name, singleton ty_name ty_ind) l in + (* check that type of constants and constructors mapped in [l] + match modulo [ind2ty] *) + let rm_impls impls (l, t) = + let rec aux impls l = match impls, l with + | Some _ :: impls, _ :: b -> aux impls b + | None :: impls, (n, a) :: b -> (n, a) :: aux impls b + | _ -> l in + aux impls l, t in + let replace m (l, t) = + let apply_m c = try CMap.find c m with Not_found -> c in + List.fold_right (fun (na, a) b -> Constr.mkProd (na, (apply_m a), b)) + l (apply_m t) in + List.iter (fun (_, cnst, tcnst, loc, indc, tindc, impls) -> + let tcnst = rm_impls impls tcnst in + let tcnst' = replace CMap.empty tcnst in + if not (Constr.equal tcnst' (replace ind2ty tindc)) then + let actual = replace CMap.empty tindc in + let expected = replace ty2ind tcnst in + warn_via_type_mismatch ?loc (env, sigma, indc, cnst, expected, actual)) + l in + (* Associate an index to each inductive, starting from 0 for [ty_ind]. *) + let ind2num, num2ind, nb_ind = + CMap.fold (fun ind _ (ind2num, num2ind, i) -> + CMap.add ind i ind2num, Int.Map.add i ind num2ind, i + 1) + (CMap.remove ty_ind constructors) + (CMap.singleton ty_ind 0, Int.Map.singleton 0 ty_ind, 1) in + (* Finally elaborate [to_post] *) + let to_post = + let rec map_prod impls tindc = match impls with + | Some _ :: impls -> ToPostHole :: map_prod impls tindc + | _ -> + match tindc with + | [] -> [] + | (_, a) :: b -> + let t = match CMap.find_opt a ind2num with + | Some i -> ToPostAs i + | None -> ToPostCopy in + let impls = match impls with [] -> [] | _ :: t -> t in + t :: map_prod impls b in + Array.init nb_ind (fun i -> + List.map (fun indc -> + let _, cnst, _, _, _, tindc, impls = List.find (eq_indc indc) l in + indc, cnst, map_prod impls (fst tindc)) + (CMap.find (Int.Map.find i num2ind) constructors)) in + (* and use constants mapped to constructors of [ty_ind] as triggers. *) + let pt_refs = List.map (fun (_, cnst, _) -> cnst) (to_post.(0)) in + to_post, pt_refs + +let locate_global_inductive allow_params qid = + let locate_param_inductive qid = + match Nametab.locate_extended qid with + | Globnames.TrueGlobal _ -> raise Not_found + | Globnames.SynDef kn -> + match Syntax_def.search_syntactic_definition kn with + | [], Notation_term.(NApp (NRef (GlobRef.IndRef i), l)) when allow_params -> + i, + List.map (function + | Notation_term.NRef r -> Some r + | Notation_term.NHole _ -> None + | _ -> raise Not_found) l + | _ -> raise Not_found in + try locate_param_inductive qid + with Not_found -> Smartlocate.global_inductive_with_alias qid, [] + +let vernac_number_notation local ty f g opts scope = + let rec parse_opts = function + | [] -> None, Nop + | h :: opts -> + let via, opts = parse_opts opts in + let via = match h, via with + | Via _, Some _ -> multiple_via_error () + | Via v, None -> Some v + | _ -> via in + let opts = match h, opts with + | After _, (Warning _ | Abstract _) -> multiple_after_error () + | After a, Nop -> a + | _ -> opts in + via, opts in + let via, opts = parse_opts opts in + (match via, opts with Some _, Abstract _ -> via_abstract_error () | _ -> ()); + let env = Global.env () in + let sigma = Evd.from_env env in + let num_ty = locate_number () in + let z_pos_ty = locate_z () in + let int63_ty = locate_int63 () in + let ty_name = ty in + let ty, via = + match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in + let tyc, params = locate_global_inductive (via = None) ty in + let to_ty = Smartlocate.global_with_alias f in + let of_ty = Smartlocate.global_with_alias g in + let cty = mkRefC ty in + let app x y = mkAppC (x,[y]) in + let arrow x y = + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) + in + let opt r = app (mkRefC (q_option ())) r in + (* Check the type of f *) + let to_kind = + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option + | _ -> + match int63_ty with + | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct + | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option + | _ -> type_error_to f ty + in + (* Check the type of g *) + let of_kind = + match num_ty with + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct + | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct + | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct + | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct + | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct + | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct + | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option + | _ -> + match z_pos_ty with + | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct + | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option + | _ -> + match int63_ty with + | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct + | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option + | _ -> type_error_of g ty + in + (match to_kind, of_kind with + | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ + | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> + warn_deprecated_decimal () + | _ -> ()); + let to_post, pt_refs = match via with + | None -> elaborate_to_post_params env sigma tyc params + | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; + warning = opts } + in + (match opts, to_kind with + | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty + | _ -> ()); + let i = + { pt_local = local; + pt_scope = scope; + pt_interp_info = NumberNotation o; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; + pt_refs; + pt_in_match = true } + in + enable_prim_token_interpretation i diff --git a/plugins/syntax/number.mli b/plugins/syntax/number.mli new file mode 100644 index 0000000000..d7d28b29ed --- /dev/null +++ b/plugins/syntax/number.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \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) *) +(************************************************************************) + +open Libnames +open Vernacexpr +open Notation + +(** * Number notation *) + +type number_string_via = qualid * (bool * qualid * qualid) list +type number_option = + | After of numnot_option + | Via of number_string_via + +val vernac_number_notation : locality_flag -> + qualid -> + qualid -> qualid -> + number_option list -> + Notation_term.scope_name -> unit + +(** These are also used in string notations *) +val locate_global_inductive : bool -> Libnames.qualid -> Names.inductive * Names.GlobRef.t option list +val elaborate_to_post_params : Environ.env -> Evd.evar_map -> Names.inductive -> Names.GlobRef.t option list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list +val elaborate_to_post_via : Environ.env -> Evd.evar_map -> Libnames.qualid -> Names.inductive -> (bool * Libnames.qualid * Libnames.qualid) list -> (Names.GlobRef.t * Names.GlobRef.t * Notation.to_post_arg list) list array * Names.GlobRef.t list diff --git a/plugins/syntax/number_string_notation_plugin.mlpack b/plugins/syntax/number_string_notation_plugin.mlpack new file mode 100644 index 0000000000..74c32d3a53 --- /dev/null +++ b/plugins/syntax/number_string_notation_plugin.mlpack @@ -0,0 +1,3 @@ +Number +String_notation +G_number_string diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml deleted file mode 100644 index 2db76719b8..0000000000 --- a/plugins/syntax/numeral.ml +++ /dev/null @@ -1,217 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) - -open Pp -open Util -open Names -open Libnames -open Constrexpr -open Constrexpr_ops -open Notation - -(** * Numeral notation *) - -let warn_abstract_large_num_no_op = - CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers" - (fun f -> - strbrk "The 'abstract after' directive has no effect when " ++ - strbrk "the parsing function (" ++ - Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++ - strbrk "option type.") - -let get_constructors ind = - let mib,oib = Global.lookup_inductive ind in - let mc = oib.Declarations.mind_consnames in - Array.to_list - (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) - -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 - | GlobRef.IndRef i -> i - | _ -> raise Not_found - -let locate_z () = - 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_numeral () = - let dint = "num.int.type" in - let duint = "num.uint.type" in - let dec = "num.decimal.type" in - let hint = "num.hexadecimal_int.type" in - let huint = "num.hexadecimal_uint.type" in - let hex = "num.hexadecimal.type" in - let int = "num.num_int.type" in - let uint = "num.num_uint.type" in - let num = "num.numeral.type" in - if Coqlib.has_ref dint && Coqlib.has_ref duint && Coqlib.has_ref dec - && Coqlib.has_ref hint && Coqlib.has_ref huint && Coqlib.has_ref hex - && Coqlib.has_ref int && Coqlib.has_ref uint && Coqlib.has_ref num - then - let q_dint = qualid_of_ref dint in - let q_duint = qualid_of_ref duint in - let q_dec = qualid_of_ref dec in - let q_hint = qualid_of_ref hint in - let q_huint = qualid_of_ref huint in - let q_hex = qualid_of_ref hex in - let q_int = qualid_of_ref int in - let q_uint = qualid_of_ref uint in - let q_num = qualid_of_ref num in - let int_ty = { - dec_int = unsafe_locate_ind q_dint; - dec_uint = unsafe_locate_ind q_duint; - hex_int = unsafe_locate_ind q_hint; - hex_uint = unsafe_locate_ind q_huint; - int = unsafe_locate_ind q_int; - uint = unsafe_locate_ind q_uint; - } in - let num_ty = { - int = int_ty; - decimal = unsafe_locate_ind q_dec; - hexadecimal = unsafe_locate_ind q_hex; - numeral = unsafe_locate_ind q_num; - } in - Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint, - num_ty, mkRefC q_num, mkRefC q_dec) - else None - -let locate_int63 () = - let int63n = "num.int63.type" in - if Coqlib.has_ref int63n - then - let q_int63 = qualid_of_ref int63n in - Some (mkRefC q_int63) - else None - -let has_type env sigma f ty = - let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in - try let _ = Constrintern.interp_constr env sigma c in true - with Pretype_errors.PretypeError _ -> false - -let type_error_to f ty = - CErrors.user_err - (pr_qualid f ++ str " should go from Numeral.int to " ++ - pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++ - fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") - -let type_error_of g ty = - CErrors.user_err - (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ - str " to Numeral.int or (option Numeral.int)." ++ fnl () ++ - str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).") - -let warn_deprecated_decimal = - CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated" - (fun () -> - strbrk "Deprecated Numeral Notation for Decimal.uint, \ - Decimal.int or Decimal.decimal. Use Numeral.uint, \ - Numeral.int or Numeral.numeral respectively.") - -let vernac_numeral_notation local ty f g scope opts = - let env = Global.env () in - let sigma = Evd.from_env env in - let num_ty = locate_numeral () in - let z_pos_ty = locate_z () in - let int63_ty = locate_int63 () in - let tyc = Smartlocate.global_inductive_with_alias ty in - let to_ty = Smartlocate.global_with_alias f in - let of_ty = Smartlocate.global_with_alias g in - let cty = mkRefC ty in - let app x y = mkAppC (x,[y]) in - let arrow x y = - mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) - in - let opt r = app (mkRefC (q_option ())) r in - let constructors = get_constructors tyc in - (* Check the type of f *) - let to_kind = - match num_ty with - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec cty) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma f (arrow cdec (opt cty)) -> Decimal num_ty, Option - | _ -> - match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct - | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option - | _ -> - match int63_ty with - | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct - | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option - | _ -> type_error_to f ty - in - (* Check the type of g *) - let of_kind = - match num_ty with - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct - | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct - | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct - | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct - | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct - | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> DecimalUInt int_ty, Option - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty cdec) -> Decimal num_ty, Direct - | Some (_, _, _, _, _, num_ty, _, cdec) when has_type env sigma g (arrow cty (opt cdec)) -> Decimal num_ty, Option - | _ -> - match z_pos_ty with - | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct - | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option - | _ -> - match int63_ty with - | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct - | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option - | _ -> type_error_of g ty - in - (match to_kind, of_kind with - | ((DecimalInt _ | DecimalUInt _ | Decimal _), _), _ - | _, ((DecimalInt _ | DecimalUInt _ | Decimal _), _) -> - warn_deprecated_decimal () - | _ -> ()); - let o = { to_kind; to_ty; of_kind; of_ty; - ty_name = ty; - warning = opts } - in - (match opts, to_kind with - | Abstract _, (_, Option) -> warn_abstract_large_num_no_op o.to_ty - | _ -> ()); - let i = - { pt_local = local; - pt_scope = scope; - pt_interp_info = NumeralNotation o; - pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; - pt_refs = constructors; - pt_in_match = true } - in - enable_prim_token_interpretation i diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli deleted file mode 100644 index 99252484b4..0000000000 --- a/plugins/syntax/numeral.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) - -open Libnames -open Vernacexpr -open Notation - -(** * Numeral notation *) - -val vernac_numeral_notation : locality_flag -> - qualid -> qualid -> qualid -> - Notation_term.scope_name -> numnot_option -> unit diff --git a/plugins/syntax/numeral_notation_plugin.mlpack b/plugins/syntax/numeral_notation_plugin.mlpack deleted file mode 100644 index f4d9cae3ff..0000000000 --- a/plugins/syntax/numeral_notation_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Numeral -G_numeral diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml deleted file mode 100644 index d66b9537b4..0000000000 --- a/plugins/syntax/r_syntax.ml +++ /dev/null @@ -1,214 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) - -open Util -open Names -open Glob_term - -(* Poor's man DECLARE PLUGIN *) -let __coq_plugin_name = "r_syntax_plugin" -let () = Mltop.add_known_module __coq_plugin_name - -exception Non_closed_number - -(**********************************************************************) -(* Parsing positive via scopes *) -(**********************************************************************) - -let binnums = ["Coq";"Numbers";"BinNums"] - -let make_dir l = DirPath.make (List.rev_map Id.of_string l) -let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) - -let is_gr c gr = match DAst.get c with -| GRef (r, _) -> GlobRef.equal r gr -| _ -> false - -let positive_modpath = MPfile (make_dir binnums) - -let positive_kn = MutInd.make2 positive_modpath (Label.make "positive") -let path_of_xI = ((positive_kn,0),1) -let path_of_xO = ((positive_kn,0),2) -let path_of_xH = ((positive_kn,0),3) -let glob_xI = GlobRef.ConstructRef path_of_xI -let glob_xO = GlobRef.ConstructRef path_of_xO -let glob_xH = GlobRef.ConstructRef path_of_xH - -let pos_of_bignat ?loc x = - let ref_xI = DAst.make @@ GRef (glob_xI, None) in - let ref_xH = DAst.make @@ GRef (glob_xH, None) in - let ref_xO = DAst.make @@ GRef (glob_xO, None) in - let rec pos_of x = - match Z.(div_rem x (of_int 2)) with - | (q,rem) when rem = Z.zero -> DAst.make @@ GApp (ref_xO,[pos_of q]) - | (q,_) when not Z.(equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q]) - | (q,_) -> ref_xH - in - pos_of x - -(**********************************************************************) -(* Printing positive via scopes *) -(**********************************************************************) - -let rec bignat_of_pos c = match DAst.get c with - | GApp (r, [a]) when is_gr r glob_xO -> Z.mul Z.(of_int 2) (bignat_of_pos a) - | GApp (r, [a]) when is_gr r glob_xI -> Z.add Z.one Z.(mul (of_int 2) (bignat_of_pos a)) - | GRef (a, _) when GlobRef.equal a glob_xH -> Z.one - | _ -> raise Non_closed_number - -(**********************************************************************) -(* Parsing Z via scopes *) -(**********************************************************************) - -let z_kn = MutInd.make2 positive_modpath (Label.make "Z") -let path_of_ZERO = ((z_kn,0),1) -let path_of_POS = ((z_kn,0),2) -let path_of_NEG = ((z_kn,0),3) -let glob_ZERO = GlobRef.ConstructRef path_of_ZERO -let glob_POS = GlobRef.ConstructRef path_of_POS -let glob_NEG = GlobRef.ConstructRef path_of_NEG - -let z_of_int ?loc n = - if not Z.(equal n zero) then - let sgn, n = - if Z.(leq zero n) then glob_POS, n else glob_NEG, Z.neg n in - DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n]) - else - DAst.make @@ GRef (glob_ZERO, None) - -(**********************************************************************) -(* Printing Z via scopes *) -(**********************************************************************) - -let bigint_of_z c = match DAst.get c with - | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a - | GApp (r,[a]) when is_gr r glob_NEG -> Z.neg (bignat_of_pos a) - | GRef (a, _) when GlobRef.equal a glob_ZERO -> Z.zero - | _ -> raise Non_closed_number - -(**********************************************************************) -(* Parsing R via scopes *) -(**********************************************************************) - -let rdefinitions = ["Coq";"Reals";"Rdefinitions"] -let r_modpath = MPfile (make_dir rdefinitions) -let r_base_modpath = MPdot (r_modpath, Label.make "RbaseSymbolsImpl") -let r_path = make_path ["Coq";"Reals";"Rdefinitions";"RbaseSymbolsImpl"] "R" - -let glob_IZR = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "IZR") -let glob_Rmult = GlobRef.ConstRef (Constant.make2 r_base_modpath @@ Label.make "Rmult") -let glob_Rdiv = GlobRef.ConstRef (Constant.make2 r_modpath @@ Label.make "Rdiv") - -let binintdef = ["Coq";"ZArith";"BinIntDef"] -let z_modpath = MPdot (MPfile (make_dir binintdef), Label.make "Z") - -let glob_pow_pos = GlobRef.ConstRef (Constant.make2 z_modpath @@ Label.make "pow_pos") - -let r_of_rawnum ?loc n = - let n,e = NumTok.Signed.to_bigint_and_exponent n in - let e,p = NumTok.(match e with EDec e -> e, 10 | EBin e -> e, 2) in - let izr z = - DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z]) in - let rmult r r' = - DAst.make @@ GApp (DAst.make @@ GRef(glob_Rmult,None), [r; r']) in - let rdiv r r' = - DAst.make @@ GApp (DAst.make @@ GRef(glob_Rdiv,None), [r; r']) in - let pow p e = - let p = z_of_int ?loc (Z.of_int p) in - let e = pos_of_bignat e in - DAst.make @@ GApp (DAst.make @@ GRef(glob_pow_pos,None), [p; e]) in - let n = - izr (z_of_int ?loc n) in - if Int.equal (Z.sign e) 1 then rmult n (izr (pow p e)) - else if Int.equal (Z.sign e) (-1) then rdiv n (izr (pow p (Z.neg e))) - else n (* e = 0 *) - -(**********************************************************************) -(* Printing R via scopes *) -(**********************************************************************) - -let rawnum_of_r c = - (* print i * 10^e, precondition: e <> 0 *) - let numTok_of_int_exp i e = - (* choose between 123e-2 and 1.23, this is purely heuristic - and doesn't play any soundness role *) - let choose_exponent = - if Int.equal (Z.sign e) 1 then - true (* don't print 12 * 10^2 as 1200 to distinguish them *) - else - let i = Z.to_string i in - let li = if i.[0] = '-' then String.length i - 1 else String.length i in - let e = Z.neg e in - let le = String.length (Z.to_string e) in - Z.(lt (add (of_int li) (of_int le)) e) in - (* print 123 * 10^-2 as 123e-2 *) - let numTok_exponent () = - NumTok.Signed.of_bigint_and_exponent i (NumTok.EDec e) in - (* print 123 * 10^-2 as 1.23, precondition e < 0 *) - let numTok_dot () = - let s, i = - if Z.sign i >= 0 then NumTok.SPlus, Z.to_string i - else NumTok.SMinus, Z.(to_string (neg i)) in - let ni = String.length i in - let e = - (Z.to_int e) in - assert (e > 0); - let i, f = - if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e - else "0", String.make (e - ni) '0' ^ i in - let i = s, NumTok.UnsignedNat.of_string i in - let f = NumTok.UnsignedNat.of_string f in - NumTok.Signed.of_int_frac_and_exponent i (Some f) None in - if choose_exponent then numTok_exponent () else numTok_dot () in - match DAst.get c with - | GApp (r, [a]) when is_gr r glob_IZR -> - let n = bigint_of_z a in - NumTok.(Signed.of_bigint CDec n) - | GApp (md, [l; r]) when is_gr md glob_Rmult || is_gr md glob_Rdiv -> - begin match DAst.get l, DAst.get r with - | GApp (i, [l]), GApp (i', [r]) - when is_gr i glob_IZR && is_gr i' glob_IZR -> - begin match DAst.get r with - | GApp (p, [t; e]) when is_gr p glob_pow_pos -> - let t = bigint_of_z t in - if not (Z.(equal t (of_int 10))) then - raise Non_closed_number - else - let i = bigint_of_z l in - let e = bignat_of_pos e in - let e = if is_gr md glob_Rdiv then Z.neg e else e in - numTok_of_int_exp i e - | _ -> raise Non_closed_number - end - | _ -> raise Non_closed_number - end - | _ -> raise Non_closed_number - -let uninterp_r (AnyGlobConstr p) = - try - Some (rawnum_of_r p) - with Non_closed_number -> - None - -open Notation - -let at_declare_ml_module f x = - Mltop.declare_cache_obj (fun () -> f x) __coq_plugin_name - -let r_scope = "R_scope" - -let _ = - register_rawnumeral_interpretation r_scope (r_of_rawnum,uninterp_r); - at_declare_ml_module enable_prim_token_interpretation - { pt_local = false; - pt_scope = r_scope; - pt_interp_info = Uid r_scope; - pt_required = (r_path,["Coq";"Reals";"Rdefinitions"]); - pt_refs = [glob_IZR; glob_Rmult; glob_Rdiv]; - pt_in_match = false } diff --git a/plugins/syntax/r_syntax.mli b/plugins/syntax/r_syntax.mli deleted file mode 100644 index b72d544151..0000000000 --- a/plugins/syntax/r_syntax.mli +++ /dev/null @@ -1,9 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \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) *) -(************************************************************************) diff --git a/plugins/syntax/r_syntax_plugin.mlpack b/plugins/syntax/r_syntax_plugin.mlpack deleted file mode 100644 index d4ee75ea48..0000000000 --- a/plugins/syntax/r_syntax_plugin.mlpack +++ /dev/null @@ -1 +0,0 @@ -R_syntax diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index e7ed0d8061..774d59dda3 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -9,21 +9,15 @@ (************************************************************************) open Pp -open Util open Names open Libnames open Constrexpr open Constrexpr_ops open Notation +open Number (** * String notation *) -let get_constructors ind = - let mib,oib = Global.lookup_inductive ind in - let mc = oib.Declarations.mind_consnames in - Array.to_list - (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) - let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -46,7 +40,7 @@ let type_error_of g ty = (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++ str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).") -let vernac_string_notation local ty f g scope = +let vernac_string_notation local ty f g via scope = let env = Global.env () in let sigma = Evd.from_env env in let app x y = mkAppC (x,[y]) in @@ -56,14 +50,16 @@ let vernac_string_notation local ty f g scope = let coption = cref (q_option ()) in let opt r = app coption r in let clist_byte = app clist cbyte in - let tyc = Smartlocate.global_inductive_with_alias ty in + let ty_name = ty in + let ty, via = + match via with None -> ty, via | Some (ty', a) -> ty', Some (ty, a) in + let tyc, params = locate_global_inductive (via = None) ty in let to_ty = Smartlocate.global_with_alias f in let of_ty = Smartlocate.global_with_alias g in let cty = cref ty in let arrow x y = mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in - let constructors = get_constructors tyc in (* Check the type of f *) let to_kind = if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct @@ -80,11 +76,10 @@ let vernac_string_notation local ty f g scope = else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option else type_error_of g ty in - let o = { to_kind = to_kind; - to_ty = to_ty; - of_kind = of_kind; - of_ty = of_ty; - ty_name = ty; + let to_post, pt_refs = match via with + | None -> elaborate_to_post_params env sigma tyc params + | Some (ty, l) -> elaborate_to_post_via env sigma ty tyc l in + let o = { to_kind; to_ty; to_post; of_kind; of_ty; ty_name; warning = () } in let i = @@ -92,7 +87,7 @@ let vernac_string_notation local ty f g scope = pt_scope = scope; pt_interp_info = StringNotation o; pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; - pt_refs = constructors; + pt_refs; pt_in_match = true } in enable_prim_token_interpretation i diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli index 0d99f98d26..f3c7c969c6 100644 --- a/plugins/syntax/string_notation.mli +++ b/plugins/syntax/string_notation.mli @@ -14,5 +14,7 @@ open Vernacexpr (** * String notation *) val vernac_string_notation : locality_flag -> - qualid -> qualid -> qualid -> + qualid -> + qualid -> qualid -> + Number.number_string_via option -> Notation_term.scope_name -> unit diff --git a/plugins/syntax/string_notation_plugin.mlpack b/plugins/syntax/string_notation_plugin.mlpack deleted file mode 100644 index 6aa081dab4..0000000000 --- a/plugins/syntax/string_notation_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -String_notation -G_string |