diff options
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | lib/genarg.ml | 12 | ||||
| -rw-r--r-- | lib/genarg.mli | 3 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 12 | ||||
| -rw-r--r-- | printing/pptactic.ml | 24 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 2 |
6 files changed, 38 insertions, 17 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 141eab3f3..29ea08e02 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -468,7 +468,7 @@ let pp_generic_argument arg = let prgenarginfo arg = let Val.Dyn (tag, _) = arg in - let tpe = Val.repr tag in + let tpe = Val.pr tag in (** FIXME *) (* try *) (* let data = Pptactic.pr_top_generic (Global.env ()) arg in *) diff --git a/lib/genarg.ml b/lib/genarg.ml index 5d5b29c99..ef0de89af 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -61,11 +61,13 @@ struct end | _ -> None - let rec repr : type a. a tag -> std_ppcmds = function - | Base t -> str (ValT.repr t) - | List t -> repr t ++ spc () ++ str "list" - | Opt t -> repr t ++ spc () ++ str "option" - | Pair (t1, t2) -> str "(" ++ repr t1 ++ str " * " ++ repr t2 ++ str ")" + let repr = ValT.repr + + let rec pr : type a. a tag -> std_ppcmds = function + | Base t -> str (repr t) + | List t -> pr t ++ spc () ++ str "list" + | Opt t -> pr t ++ spc () ++ str "option" + | Pair (t1, t2) -> str "(" ++ pr t1 ++ str " * " ++ pr t2 ++ str ")" end diff --git a/lib/genarg.mli b/lib/genarg.mli index 6cc7893dc..93665fd45 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -99,7 +99,8 @@ sig type t = Dyn : 'a tag * 'a -> t val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option - val repr: 'a tag -> Pp.std_ppcmds + val repr : 'a typ -> string + val pr : 'a tag -> Pp.std_ppcmds end (** Dynamic types for toplevel values. While the generic types permit to relate diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4c74984f8..6f0297268 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -65,7 +65,7 @@ let val_tag wit = val_tag (topwit wit) let pr_argument_type arg = let Val.Dyn (tag, _) = arg in - Val.repr tag + Val.pr tag let safe_msgnl s = Proofview.NonLogical.catch @@ -83,9 +83,9 @@ let push_appl appl args = match appl with | UnnamedAppl -> UnnamedAppl | GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l) -let pr_generic arg = (** FIXME *) +let pr_generic arg = let Val.Dyn (tag, _) = arg in - str"<" ++ Val.repr tag ++ str ">" + str"<" ++ Val.pr tag ++ str ":(" ++ Pptactic.pr_value Pptactic.ltop arg ++ str ")>" let pr_appl h vs = Pptactic.pr_ltac_constant h ++ spc () ++ Pp.prlist_with_sep spc pr_generic vs @@ -148,9 +148,9 @@ module Value = struct of_tacvalue closure let cast_error wit v = - let pr_v = mt () in (** FIXME *) + let pr_v = Pptactic.pr_value Pptactic.ltop v in let Val.Dyn (tag, _) = v in - let tag = Val.repr tag in + let tag = Val.pr tag in errorlabstrm "" (str "Type error: value " ++ pr_v ++ str "is a " ++ tag ++ str " while type " ++ Genarg.pr_argument_type (unquote (rawwit wit)) ++ str " was expected.") @@ -198,7 +198,7 @@ module Value = struct end -let print_top_val env v = mt () (** FIXME *) +let print_top_val env v = Pptactic.pr_value Pptactic.ltop v let dloc = Loc.ghost diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c175b206d..355a6a7d6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -106,7 +106,23 @@ module Make let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let pr_value _ _ = str "(* FIXME *)" + let rec pr_value lev (Val.Dyn (tag, x)) : std_ppcmds = match tag with + | Val.List tag -> + pr_sequence (fun x -> pr_value lev (Val.Dyn (tag, x))) x + | Val.Opt tag -> pr_opt (fun x -> pr_value lev (Val.Dyn (tag, x))) x + | Val.Pair (tag1, tag2) -> + str "(" ++ pr_value lev (Val.Dyn (tag1, fst x)) ++ str ", " ++ + pr_value lev (Val.Dyn (tag1, fst x)) ++ str ")" + | Val.Base t -> + let name = Val.repr t in + let default = str "<" ++ str name ++ str ">" in + match ArgT.name name with + | None -> default + | Some (ArgT.Any arg) -> + let wit = ExtraArg arg in + match Val.eq (val_tag (Topwit wit)) (Val.Base t) with + | None -> default + | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) let pr_with_occurrences pr (occs,c) = match occs with @@ -1245,7 +1261,7 @@ module Make let typed_printers = (strip_prod_binders_constr) in - let prtac n (t:tactic_expr) = + let rec prtac n (t:tactic_expr) = let pr = { pr_tactic = pr_glob_tactic_level env; pr_constr = pr_constr_env env Evd.empty; @@ -1261,10 +1277,10 @@ module Make pr_value pr_constr_pattern; pr_extend = pr_extend_rec (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern; + prtac pr_constr_pattern; pr_alias = pr_alias (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) - pr_value pr_constr_pattern; + prtac pr_constr_pattern; } in make_pr_tac diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index b98b6c67e..95cf541fd 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -72,4 +72,6 @@ module type Pp = sig val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('b, 'a) match_rule -> std_ppcmds + val pr_value : tolerability -> Val.t -> std_ppcmds + end |