From 565a9a1b5368c586e529fc9774e4cb4b81c6441b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 31 Oct 2017 17:18:50 +0100 Subject: Setting a system to register printers for Ltac values. The model provides three kinds of printers depending on whether the printer needs a context, and, if yes if it supports levels. In the latter case, it takes defaults levels for printing when in a surrounded context (lconstr style) and for printing when not in a surrounded context (constr style). This model preserves the 8.7 focussing semantics of "idtac" (i.e. focussing only when an env is needed) but it also shows that the semantics of "idtac", which focusses the goal depending on the type of its arguments, is a bit ad hoc to understand. See discussion at PR#6047 "https://github.com/coq/coq/pull/6047#discussion_r148278454". --- plugins/ltac/tacinterp.ml | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 66f124d2d1..ec8777a45c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -76,6 +76,9 @@ let out_gen wit v = let val_tag wit = val_tag (topwit wit) +let base_val_typ wit = + match val_tag wit with Val.Base t -> t | _ -> anomaly (str "Not a base val.") + let pr_argument_type arg = let Val.Dyn (tag, _) = arg in Val.pr tag @@ -124,6 +127,8 @@ type tacvalue = 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 "")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v -- cgit v1.2.3 From 9c232079b996313ed1f5b63746304ccd639c8355 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 29 Oct 2017 19:22:27 +0100 Subject: Binding ltac printing functions to the system of generic printing. This concerns pr_value and message_of_value. This has a few consequences. For instance, no more ad hoc message "a term" or "a tactic", when not enough information is available for printing, one gets a generic message "a value of type foobar". But we also have more printers, satisfying e.g. request #5786. --- plugins/ltac/tacinterp.ml | 79 +++++++++++------------------------------------ 1 file changed, 18 insertions(+), 61 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index ec8777a45c..8b90a0188c 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -236,24 +236,16 @@ let curr_debug ist = match TacStore.get ist.extra f_debug with (* Displays a value *) let pr_value env v = let v = Value.normalize v in - if has_type v (topwit wit_tacvalue) then str "a tactic" - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in + let pr_with_env pr = match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr) then - let c = out_gen (topwit wit_constr) v in - match env with - | Some (env,sigma) -> pr_leconstr_env env sigma c - | _ -> str "a term" - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - match env with - | Some (env,sigma) -> pr_lconstr_under_binders_env env sigma c - | _ -> str "a term" - else - str "a value of type" ++ spc () ++ pr_argument_type v + | Some (env,sigma) -> pr env sigma + | 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 } -> + pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = let pp_body = Pptactic.pr_glob_tactic env body in @@ -823,51 +815,16 @@ let interp_constr_may_eval ist env sigma c = end (** TODO: should use dedicated printers *) -let rec message_of_value v = +let message_of_value v = let v = Value.normalize v in - let open Ftactic in - if has_type v (topwit wit_tacvalue) then - Ftactic.return (str "") - else if has_type v (topwit wit_constr) then - let v = out_gen (topwit wit_constr) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end - else if has_type v (topwit wit_constr_under_binders) then - let c = out_gen (topwit wit_constr_under_binders) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_constr_under_binders_env (pf_env gl) (project gl) c) - end - else if has_type v (topwit wit_unit) then - Ftactic.return (str "()") - else if has_type v (topwit wit_int) then - Ftactic.return (int (out_gen (topwit wit_int) v)) - else if has_type v (topwit wit_intro_pattern) then - let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = - let (sigma, c) = c env sigma in - pr_econstr_env env sigma c - in - Ftactic.enter begin fun gl -> - Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) - end - else if has_type v (topwit wit_constr_context) then - let c = out_gen (topwit wit_constr_context) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) c) end - else if has_type v (topwit wit_uconstr) then - let c = out_gen (topwit wit_uconstr) v in - Ftactic.enter begin fun gl -> - Ftactic.return (pr_closed_glob_env (pf_env gl) - (project gl) c) - end - else if has_type v (topwit wit_var) then - let id = out_gen (topwit wit_var) v in - Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end - else match Value.to_list v with - | Some l -> - Ftactic.List.map message_of_value l >>= fun l -> - Ftactic.return (prlist_with_sep spc (fun x -> x) l) - | None -> - let tag = pr_argument_type v in - Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *) + let pr_with_env pr = + 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 } -> + pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) -- cgit v1.2.3 From d073a70d84aa6802a03d03a17d2246d607e85db1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 30 Oct 2017 10:35:13 +0100 Subject: Ltac Debug: exporting env and sigma when needed so that term can be printed. We do it so as to preserve non-focussing semantics for non-focussing generic arguments. This assumes that the code treats them consistently, which is not enforced statically, but which is reasonable in the sense that when we need a context for printing, we have no other choice as needing a context and we needed one also at interpretation time. --- plugins/ltac/tacinterp.ml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8b90a0188c..fd75862c6f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -908,13 +908,13 @@ let interp_in_hyp_as ist env sigma (id,ipat) = let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in sigma,(interp_hyp ist env sigma id,ipat) -let interp_binding_name ist sigma = function +let interp_binding_name ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function @@ -926,7 +926,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function let interp_binding ist env sigma (loc,(b,c)) = let sigma, c = interp_open_constr ist env sigma c in - sigma, (loc,(interp_binding_name ist sigma b,c)) + sigma, (loc,(interp_binding_name ist env sigma b,c)) let interp_bindings ist env sigma = function | NoBindings -> @@ -1348,10 +1348,14 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = end >>= fun v -> (* No errors happened, we propagate the trace *) let v = append_trace trace v in - Proofview.tclLIFT begin - debugging_step ist - (fun () -> - str"evaluation returns"++fnl()++pr_value None v) + let call_debug env = + Proofview.tclLIFT (debugging_step ist (fun () -> str"evaluation returns"++fnl()++pr_value env v)) in + begin + let open Genprint in + match generic_val_print v with + | PrinterBasic _ -> call_debug None + | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + 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 else -- cgit v1.2.3