diff options
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 102 |
1 files changed, 34 insertions, 68 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 66f124d2d..fd75862c6 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 "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -231,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 - 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 + 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_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 @@ -818,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 "<tactic>") - 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) @@ -946,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 @@ -964,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 -> @@ -1386,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 |