diff options
Diffstat (limited to 'plugins')
29 files changed, 371 insertions, 190 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index fb65a8639a..c8c4c2dad9 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -38,9 +38,8 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> + let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 9cbc3fd713..5d0f9c167e 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -100,11 +100,41 @@ let pp_global k r = str (str_global k r) let pp_modname mp = str (Common.pp_module mp) +(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *) + +let infix_symbols = + ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ] +let operator_chars = + [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ] + +(* infix ops in OCaml, but disallowed by preceding grammar *) + +let builtin_infixes = + [ "::" ; "," ] + +let substring_all_opchars s start stop = + let rec check_char i = + if i >= stop then true + else + List.mem s.[i] operator_chars && check_char (i+1) + in + check_char start + let is_infix r = is_inline_custom r && (let s = find_custom r in - let l = String.length s in - l >= 2 && s.[0] == '(' && s.[l-1] == ')') + let len = String.length s in + len >= 3 && + (* parenthesized *) + (s.[0] == '(' && s.[len-1] == ')' && + let inparens = String.trim (String.sub s 1 (len - 2)) in + let inparens_len = String.length inparens in + (* either, begins with infix symbol, any remainder is all operator chars *) + (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) || + (* or, starts with #, at least one more char, all are operator chars *) + (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) || + (* or, is an OCaml built-in infix *) + (List.mem inparens builtin_infixes))) let get_infix r = let s = find_custom r in diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 938bec25b9..b81010c7bd 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -40,17 +40,17 @@ let _= in declare_int_option gdopt -let congruence_depth=ref 100 let _= + let congruence_depth=ref 100 in let gdopt= - { optdepr=false; + { optdepr=true; (* noop *) optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function - None->congruence_depth:=0 + None->congruence_depth:=0 | Some i->congruence_depth:=(max i 0))} in declare_int_option gdopt diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71e..87609296bc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index fa43536304..889c064b24 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1497,7 +1497,7 @@ let do_build_inductive let _time2 = System.get_time () in try with_full_print - (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) + (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false)) Decl_kinds.Finite with | UserError(s,msg) as e -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad3063..071599d9c5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in - let evdref = ref (Evd.from_env env0) in - let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) @@ -406,7 +406,8 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp match fixpoint_exprl with | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in - Command.do_definition + ComDefinition.do_definition + ~program_mode:false fname (Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); @@ -426,7 +427,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> @@ -616,8 +617,8 @@ and rebuild_nal aux bk bl' nal typ = let rebuild_bl aux bl typ = rebuild_bl aux bl typ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = - let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in - let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in + let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in + let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in let constr_expr_typel = with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in let fixpoint_exprl_with_new_bl = diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8bf6e48fdb..5a9248d478 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -183,7 +183,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -197,6 +199,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +209,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 9e2774ff32..9fcb35f89e 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive) } in *) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) - let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,pl,impls = Command.interp_mutual_inductive indl [] + let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in + let mie,pl,impls = ComInductive.interp_mutual_inductive indl [] false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) - ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls) + ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls) (* Find infos on identifier id. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b7..363ad5dfc9 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = @@ -1423,7 +1427,7 @@ let com_terminate nb_args ctx hook = let start_proof ctx (tac_start:tactic) (tac_end:tactic) = - let evmap, env = Pfedit.get_current_context () in + let evd, env = Pfedit.get_current_context () in Lemmas.start_proof thm_name (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env) ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) hook; @@ -1475,13 +1479,13 @@ let (com_eqn : int -> Id.t -> | ConstRef c -> is_opaque_constant c | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in - let evmap, env = Pfedit.get_current_context () in - let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in + let evd, env = Pfedit.get_current_context () in + let evd = Evd.from_ctx (Evd.evar_universe_context evd) in let f_constr = constr_of_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in (Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign:(Environ.named_context_val env) - evmap + evd (EConstr.of_constr equation_lemma_type) (Lemmas.mk_hook (fun _ _ -> ())); ignore (by @@ -1524,14 +1528,14 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let open Constr in let open CVars in let env = Global.env() in - let evd = ref (Evd.from_env env) in - let function_type = interp_type_evars env evd type_of_f in + let evd = Evd.from_env env in + let evd, function_type = interp_type_evars env evd type_of_f in let function_type = EConstr.Unsafe.to_constr function_type in let env = push_named (Context.Named.Declaration.LocalAssum (function_name,function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) - let ty = interp_type_evars env evd ~impls:rec_impls eq in + let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in let ty = EConstr.Unsafe.to_constr ty in - let evm, nf = Evarutil.nf_evars_and_universes !evd in + let evd, nf = Evarutil.nf_evars_and_universes evd in let equation_lemma_type = nf_betaiotazeta (EConstr.of_constr (nf ty)) in let function_type = nf function_type in let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in @@ -1556,16 +1560,16 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = - let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in + let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evd) in declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res in (* Refresh the global universes, now including those of _F *) - let evm = Evd.from_env (Global.env ()) in + let evd = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in let relation, evuctx = - interp_constr env_with_pre_rec_args evm r + interp_constr env_with_pre_rec_args evd r in - let evm = Evd.from_ctx evuctx in + let evd = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref Undefined in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) @@ -1595,7 +1599,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num and functional_ref = destConst (constr_of_global functional_ref) and eq_ref = destConst (constr_of_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr - functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evm (EConstr.of_constr res)) (EConstr.of_constr relation); + functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) (nb_prod evd (EConstr.of_constr res)) (EConstr.of_constr relation); Flags.if_verbose msgnl (h 1 (Ppconstr.pr_id function_name ++ spc () ++ str"is defined" )++ fnl () ++ @@ -1614,5 +1618,5 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num term_id using_lemmas (List.length res_vars) - evm (Lemmas.mk_hook hook)) + evd (Lemmas.mk_hook hook)) () diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175b..ebf6e450b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -242,12 +237,7 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: @@ -471,7 +461,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d707512457..e5ff473568 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,24 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function | ListArg t -> aux t ^ "_list" @@ -127,9 +145,9 @@ let string_of_genarg_arg (ArgumentType arg) = | Some Refl -> let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -508,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function @@ -723,8 +739,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -1192,42 +1210,77 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = - Genprint.PrinterNeedsContext (fun env sigma -> + Genprint.TopPrinterNeedsContext (fun env sigma -> h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = + let env = Global.env () in + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + in + Genprint.register_print0 wit f g h + let declare_extra_vernac_genarg_pprule wit f = - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) -let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in Miscprint.pr_intro_pattern print_constr p) -let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) -let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in Miscprint.pr_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in pr_with_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, c = match c with | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) | clear_flag,ElimOnAnonHyp n as x -> sigma, x @@ -1236,12 +1289,16 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) let make_constr_printer f c = - Genprint.PrinterNeedsContextAndLevel { + Genprint.TopPrinterNeedsContextAndLevel { Genprint.default_already_surrounded = Ppconstr.ltop; Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac c = @@ -1255,80 +1312,81 @@ let pr_lglob_constr_pptac c = let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) (lift int); - Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); - Genprint.register_print0 wit_ident - pr_id pr_id (lift pr_id); - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) (lift pr_id); - Genprint.register_print0 + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_bindings_env ; - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 wit_open_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_destruction_arg_env ; - Genprint.register_print0 Stdarg.wit_int int int (lift int); - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); - Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); - Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5ecfaf590c..bda5774abf 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -40,12 +40,37 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_genarg_pprule_with_level : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer_with_level -> + 'b glob_extra_genarg_printer_with_level -> + 'c extra_genarg_printer_with_level -> + (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> unit diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9ae8bfe65b..5e3b7cf775 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -289,7 +289,7 @@ let rec find_in_stack what acc = function | { name } as x :: rest when String.equal name what -> Some(acc, x, rest) | { name } as x :: rest -> find_in_stack what (x :: acc) rest -let exit_tactic start_time c = +let exit_tactic ~count_call start_time c = let diff = time () -. start_time in match Local.(!stack) with | [] | [_] -> @@ -304,7 +304,7 @@ let exit_tactic start_time c = let node = { node with total = node.total +. diff; local = node.local +. diff; - ncalls = node.ncalls + 1; + ncalls = node.ncalls + (if count_call then 1 else 0); max_total = max node.max_total diff; } in (* updating the stack *) @@ -341,7 +341,7 @@ let tclFINALLY tac (finally : unit Proofview.tactic) = (fun v -> finally <*> Proofview.tclUNIT v) (fun (exn, info) -> finally <*> Proofview.tclZERO ~info exn) -let do_profile s call_trace tac = +let do_profile s call_trace ?(count_call=true) tac = let open Proofview.Notations in Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> if !is_profiling then @@ -359,7 +359,7 @@ let do_profile s call_trace tac = tac (Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> (match call_trace with - | (_, c) :: _ -> exit_tactic start_time c + | (_, c) :: _ -> exit_tactic ~count_call start_time c | [] -> ())))) | None -> tac @@ -408,7 +408,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_notice (to_string ~cutoff ~filter results) + Feedback.msg_info (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index 52827cb36b..feb7773526 100644 --- a/plugins/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli @@ -9,9 +9,39 @@ (** Ltac profiling primitives *) +(* Note(JasonGross): Ltac semantics are a bit insane. There isn't + really a good notion of how many times a tactic has been "called", + because tactics can be partially evaluated, and it's unclear + whether the number of "calls" should be the number of times the + body is fetched and unfolded, or the number of times the code is + executed to a value, etc. The logic in [Tacinterp.eval_tactic] + gives a decent approximation, which I believe roughly corresponds + to the number of times that the engine runs the tactic value which + results from evaluating the tactic expression bound to the name + we're considering. However, this is a poor approximation of the + time spent in the tactic; we want to consider time spent evaluating + a tactic expression to a tactic value to be time spent in the + expression, not just time spent in the caller of the expression. + So we need to wrap some nodes in additional profiling calls which + don't count towards to total call count. Whether or not a call + "counts" is indicated by the [count_call] boolean argument. + + Unfortunately, at present, we can get very strange call graphs when + a named tactic expression never runs as a tactic value: if we have + [Ltac t0 := t.] and [Ltac t1 := t0.], then [t1] is considered to + run 0(!) times. It evaluates to [t] during tactic expression + evaluation, and although the call trace records the fact that it + was called by [t0] which was called by [t1], the tactic running + phase never sees this. Thus we get one call tree (from expression + evaluation) that has [t1] calls [t0] calls [t], and another call + tree which says that the caller of [t1] calls [t] directly; the + expression evaluation time goes in the first tree, and the call + count and tactic running time goes in the second tree. Alas, I + suspect that fixing this requires a redesign of how the profiler + hooks into the tactic engine. *) val do_profile : string -> ('a * Tacexpr.ltac_call_kind) list -> - 'b Proofview.tactic -> 'b Proofview.tactic + ?count_call:bool -> 'b Proofview.tactic -> 'b Proofview.tactic val set_profiling : bool -> unit @@ -46,4 +76,3 @@ type treenode = { (* Returns the profiling results known by the current process *) val get_local_profiling_results : unit -> treenode val feedback_results : treenode -> unit - diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 2b1106ee21..f095660638 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -13,7 +13,7 @@ open Profile_ltac open Stdarg -DECLARE PLUGIN "profile_ltac_plugin" +DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) @@ -22,7 +22,7 @@ TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END -TACTIC EXTEND stop_profiling +TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index c0060c5a7c..a698b05dd7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -361,8 +361,8 @@ end) = struct end (* let my_type_of env evars c = Typing.e_type_of env evars c *) -(* let mytypeofkey = Profile.declare_profile "my_type_of";; *) -(* let my_type_of = Profile.profile3 mytypeofkey my_type_of *) +(* let mytypeofkey = CProfile.declare_profile "my_type_of";; *) +(* let my_type_of = CProfile.profile3 mytypeofkey my_type_of *) let type_app_poly env env evd f args = @@ -1781,7 +1781,9 @@ let declare_an_instance n s args = let declare_instance a aeq n s = declare_an_instance n s [a;aeq] let anew_instance global binders instance fields = - new_instance (Flags.is_universe_polymorphism ()) + let program_mode = Flags.is_program_mode () in + let poly = Flags.is_universe_polymorphism () in + new_instance ~program_mode poly binders instance (Some (true, CAst.make @@ CRecord (fields))) ~global ~generalize:false ~refine:false Hints.empty_hint_info @@ -2012,23 +2014,26 @@ let add_morphism glob binders m s n = [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in - ignore(new_instance ~global:glob poly binders instance - (Some (true, CAst.make @@ CRecord [])) - ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) + let program_mode = Flags.is_program_mode () in + ignore(new_instance ~program_mode ~global:glob poly binders instance + (Some (true, CAst.make @@ CRecord [])) + ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info) (** Bind to "rewrite" too *) (** Taken from original setoid_replace, to emulate the old rewrite semantics where lemmas are first instantiated and then rewrite proceeds. *) -let check_evar_map_of_evars_defs evd = +let check_evar_map_of_evars_defs env evd = let metas = Evd.meta_list evd in let check_freemetas_is_empty rebus = Evd.Metaset.iter (fun m -> - if Evd.meta_defined evd m then () else - raise - (Logic.RefinerError (Logic.UnresolvedBindings [Evd.meta_name evd m]))) + if Evd.meta_defined evd m then () + else begin + raise + (Logic.RefinerError (env, evd, Logic.UnresolvedBindings [Evd.meta_name evd m])) + end) in List.iter (fun (_,binding) -> @@ -2063,7 +2068,7 @@ let unification_rewrite l2r c1 c2 sigma prf car rel but env = let c1 = if l2r then nf c' else nf c1 and c2 = if l2r then nf c2 else nf c' and car = nf car and rel = nf rel in - check_evar_map_of_evars_defs sigma; + check_evar_map_of_evars_defs env sigma; let prf = nf prf in let prfty = nf (Retyping.get_type_of env sigma prf) in let sort = sort_of_rel env sigma but in @@ -2084,8 +2089,8 @@ let get_hyp gl (c,l) clause l2r = let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -(* let rewriteclaustac_key = Profile.declare_profile "cl_rewrite_clause_tac";; *) -(* let cl_rewrite_clause_tac = Profile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) +(* let rewriteclaustac_key = CProfile.declare_profile "cl_rewrite_clause_tac";; *) +(* let cl_rewrite_clause_tac = CProfile.profile5 rewriteclaustac_key cl_rewrite_clause_tac *) (** Setoid rewriting when called with "rewrite" *) let general_s_rewrite cl l2r occs (c,l) ~new_goals = diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index c03a867326..9ae112d371 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) (fun c -> - Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in + Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9bd3efc6b7..ccd555b615 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index b16b0a7bae..ebffde441d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 1a8ec6d6f6..179952f28b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -242,9 +242,9 @@ let pr_value env v = | None -> str "a value of type" ++ spc () ++ pr_argument_type v in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = @@ -420,7 +420,7 @@ let interp_hyp ist env sigma (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else Loc.raise ?loc (Logic.RefinerError (Logic.NoSuchHyp id)) + else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) let interp_hyp_list_as_list ist env sigma (loc,id as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) @@ -821,9 +821,9 @@ let message_of_value v = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> Ftactic.return (pr ()) - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> Ftactic.return (pr ()) + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function @@ -890,7 +890,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar (loc,id)) -> - (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with + (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) @@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) @@ -1272,7 +1272,8 @@ 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; extra = extra; } in let appl = GlbAppl[r,[]] in - val_interp ~appl ist (Tacenv.interp_ltac r) + Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false + (val_interp ~appl ist (Tacenv.interp_ltac r)) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1338,7 +1339,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = let ist = { lfun = newlfun; extra = TacStore.set ist.extra f_trace []; } in - catch_error_tac trace (val_interp ist body) >>= fun v -> + Profile_ltac.do_profile "interp_app" trace ~count_call:false + (catch_error_tac trace (val_interp ist body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> @@ -1353,8 +1355,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = begin let open Genprint in match generic_val_print v with - | PrinterBasic _ -> call_debug None - | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + | TopPrinterBasic _ -> call_debug None + | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ -> Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval @@ -1380,13 +1382,38 @@ and tactic_of_value ist vle = extra = TacStore.set ist.extra f_trace []; } in let tac = name_if_glob appl (eval_tactic ist t) in Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac) - | VFun (_, _, _,vars,_) -> - let numargs = List.length vars in - Tacticals.New.tclZEROMSG - (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ - Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ - Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum Name.print vars ++ Pp.str ".") + | VFun (appl,_,vmap,vars,_) -> + let tactic_nm = + match appl with + UnnamedAppl -> "An unnamed user-defined tactic" + | GlbAppl apps -> + let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + match nms with + [] -> assert false + | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) + in + let numargs = List.length vars in + let givenargs = + List.map (fun (arg,_) -> Names.Id.to_string arg) (Names.Id.Map.bindings vmap) in + let numgiven = List.length givenargs in + Tacticals.New.tclZEROMSG + (Pp.str tactic_nm ++ Pp.str " was not fully applied:" ++ spc() ++ + (match numargs with + 0 -> assert false + | 1 -> + Pp.str "There is a missing argument for variable " ++ + (Name.print (List.hd vars)) + | _ -> Pp.str "There are missing arguments for variables " ++ + pr_enum Name.print vars) ++ Pp.pr_comma () ++ + match numgiven with + 0 -> + Pp.str "no arguments at all were provided." + | 1 -> + Pp.str "an argument was provided for variable " ++ + Pp.str (List.hd givenargs) ++ Pp.str "." + | _ -> + Pp.str "arguments were provided for variables " ++ + pr_enum Pp.str givenargs ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faebe..79bf3685e2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e5907..e87951dd7f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c1..387a525141 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 337510ef1f..0d491d92bd 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -155,7 +155,7 @@ let mk_list univ typ l = loop l let mk_plist = - let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in + let type1lev = Universes.new_univ_level () in fun l -> mk_list type1lev mkProp l let mk_list = mk_list Univ.Level.set diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index f22f00839a..e3e749b754 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,8 @@ let ic_unsafe c = (*FIXME remove *) let decl_constant na univs c = let open Constr in - let vars = Univops.universes_of_constr c in + let env = Global.env () in + let vars = Univops.universes_of_constr env c in let univs = Univops.restrict_universe_context univs vars in let univs = Monomorphic_const_entry univs in mkConst(declare_constant (Id.of_string na) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 047ca509be..8493dbdbb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index bd9633afbd..6032ed2af8 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,14 +143,14 @@ let newssrcongrtac arg ist gl = (** Coq rewrite compatibility flag *) -let ssr_strict_match = ref false let _ = - Goptions.declare_bool_option + let ssr_strict_match = ref false in + Goptions.declare_bool_option { Goptions.optname = "strict redex matching"; Goptions.optkey = ["Match"; "Strict"]; Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = false; + Goptions.optdepr = true; (* noop *) Goptions.optwrite = (fun b -> ssr_strict_match := b) } (** Rewrite rules *) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7385ed84c7..4f530a0aec 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d )) + Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), + ((Loc.tag s),None),(d ))) ]]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e63a05b781..d6dbad7a95 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1228,7 +1228,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1 + | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1236,8 +1236,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in let concl = find_T env0 concl0 1 ~k:do_subst in - let _ = end_T () in - concl + let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> let p = fs sigma p in let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in @@ -1252,8 +1252,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env _ -> do_subst env e_body))) in - let _ = end_X () in let _ = end_T () in - concl + let _ = end_X () in let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, E_In_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1268,8 +1268,9 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> find_E env e_body h ~k:do_subst))) in - let _ = end_E () in let _ = end_X () in let _ = end_T () in - concl + let _,_,(_,us,_) = end_E () in + let _ = end_X () in let _ = end_T () in + concl, us | Some (sigma, E_As_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1287,8 +1288,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in - let _ = end_X () in let _ = end_TE () in - concl + let _ = end_X () in let _,_,(_,us,_) = end_TE () in + concl, us ;; let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = @@ -1306,12 +1307,14 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in (fun env c _ h' -> - do_once r (fun () -> c, Evd.empty_evar_universe_context); + do_once r (fun () -> c); if do_make_rel then mkRel (h'+h-1) else c), - (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in - let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + (fun _ -> if !r = None then fst(redex_of_pattern env pat) + else assert_done r) in + let cl, us = + eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in let e = conclude cl in - e, cl + (e, us), cl ;; (* clenup interface for external use *) @@ -1319,6 +1322,10 @@ let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + fst (eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst) +;; + let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let p = EConstr.Unsafe.to_constr p in let concl = EConstr.Unsafe.to_constr concl in |